diff options
| author | Gaëtan Gilbert | 2017-10-12 13:55:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (patch) | |
| tree | b177cc86b2742893adf0b181e53c03b8897b48cc /tactics | |
| parent | 6c447d7a7190857b03bb2992f443f1b818618a94 (diff) | |
Make Sorts.t private
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eqschemes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 3c1115d056..5dd55b8a9f 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -789,7 +789,7 @@ let build_congr env (eq,refl,ctx) ind = let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt - (mkNamedLambda varB (mkSort (Type uni)) + (mkNamedLambda varB (mkType uni) (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB)) (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign) (mkNamedLambda varH |