diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-18 20:35:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:53 +0100 |
| commit | 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 (patch) | |
| tree | f1ef11f826c498a78c9af6ffd9020fbc454dcd5e /engine/eConstr.ml | |
| parent | 8b660087beb2209e52bc4412dc82c6727963c6a5 (diff) | |
Equality API using EConstr.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 9e0a55a0d..1dd9d0c00 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -78,6 +78,8 @@ type cofixpoint = (t, t) pcofixpoint type unsafe_judgment = (constr, types) Environ.punsafe_judgment type unsafe_type_judgment = types Environ.punsafe_type_judgment +let in_punivs a = (a, Univ.Instance.empty) + let mkProp = of_kind (Sort Sorts.prop) let mkSet = of_kind (Sort Sorts.set) let mkType u = of_kind (Sort (Sorts.Type u)) @@ -92,8 +94,11 @@ let mkLambda (na, t, c) = of_kind (Lambda (na, t, c)) let mkLetIn (na, b, t, c) = of_kind (LetIn (na, b, t, c)) let mkApp (f, arg) = of_kind (App (f, arg)) let mkConstU pc = of_kind (Const pc) +let mkConst c = of_kind (Const (in_punivs c)) let mkIndU pi = of_kind (Ind pi) +let mkInd i = of_kind (Ind (in_punivs i)) let mkConstructU pc = of_kind (Construct pc) +let mkConstruct c = of_kind (Construct (in_punivs c)) 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) |