diff options
| author | Gaëtan Gilbert | 2017-10-31 17:04:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 23f84f37c674a07e925925b7e0d50d7ee8414093 (patch) | |
| tree | 7e470de5769c994d8df37c44fed12cf299d5b194 /engine/eConstr.ml | |
| parent | 75508769762372043387c67a9abe94e8f940e80a (diff) | |
Add relevance marks on binders.
Kernel should be mostly correct, higher levels do random stuff at
times.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 521d6b707d..981f9454e4 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -73,7 +73,8 @@ let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p)) let mkFix f = of_kind (Fix f) let mkCoFix f = of_kind (CoFix f) let mkProj (p, c) = of_kind (Proj (p, c)) -let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2)) +let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2)) +let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2 let mkInt i = of_kind (Int i) let mkRef (gr,u) = let open GlobRef in match gr with @@ -668,9 +669,9 @@ let mkLambda_or_LetIn decl c = | LocalAssum (na,t) -> mkLambda (na, t, c) | LocalDef (na,b,t) -> mkLetIn (na, b, t, c) -let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c) -let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c) -let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2) +let mkNamedProd id typ c = mkProd (map_annot Name.mk_name id, typ, Vars.subst_var id.binder_name c) +let mkNamedLambda id typ c = mkLambda (map_annot Name.mk_name id, typ, Vars.subst_var id.binder_name c) +let mkNamedLetIn id c1 t c2 = mkLetIn (map_annot Name.mk_name id, c1, t, Vars.subst_var id.binder_name c2) let mkNamedProd_or_LetIn decl c = let open Context.Named.Declaration in |