diff options
| author | Gaëtan Gilbert | 2017-10-27 14:03:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 75508769762372043387c67a9abe94e8f940e80a (patch) | |
| tree | 3f63e7790e9f3b6e7384b0a445d62cfa7edbe829 /tactics | |
| parent | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (diff) | |
Add a non-cumulative impredicative universe SProp.
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eqschemes.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 5dd55b8a9f..554fe3cbed 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -66,7 +66,7 @@ module RelDecl = Context.Rel.Declaration let hid = Id.of_string "H" let xid = Id.of_string "X" -let default_id_of_sort = function InProp | InSet -> hid | InType -> xid +let default_id_of_sort = function InSProp | InProp | InSet -> hid | InType -> xid let fresh env id = next_global_ident_away id Id.Set.empty let with_context_set ctx (b, ctx') = (b, Univ.ContextSet.union ctx ctx') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 415225454a..ee9d117d4d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -947,7 +947,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | Evar ev when force_flag -> - let sigma, t = Evardefine.define_evar_as_product sigma ev in + let sigma, t = Evardefine.define_evar_as_product env sigma ev in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (intro_then_gen name_flag move_flag force_flag dep_flag tac) |