More unified All_local_env, cleaned up {PCUIC,}Typing

MetaCoq · Nov 7, 2023 · 9d8924c · 9d8924c
1 parent 5ee800e
commit 9d8924c
Show file tree

Hide file tree

Showing 35 changed files with 479 additions and 733 deletions.
diff --git a/common/theories/BasicAst.v b/common/theories/BasicAst.v
@@ -244,6 +244,10 @@ End Contexts.
 
 Arguments context_decl : clear implicits.
 
+Definition judgment_of_decl {term universe} d : judgment_ term universe :=
+  TermoptTyp (decl_body d) (decl_type d).
+
+
 Definition map_decl {term term'} (f : term -> term') (d : context_decl term) : context_decl term' :=
   {| decl_name := d.(decl_name);
      decl_body := option_map f d.(decl_body);