diff options
| author | Arnaud Spiwack | 2014-10-21 20:47:32 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-22 07:31:44 +0200 |
| commit | 81b812c0512fb61342e3f43ebc29bf843a079321 (patch) | |
| tree | 518a3e81749db570b7fc1a65be19f1e586cf3ffe /tactics | |
| parent | 9f0f12e4aa2934283fd3fb3c61f977081cb99a3a (diff) | |
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index c09a22c310..b55ee7030b 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1804,7 +1804,7 @@ let add_morphism_infer glob m n = let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = build_morphism_signature m in - let ctx = Evd.empty_evar_universe_context (*FIXME *) in + let evd = Evd.empty (*FIXME *) in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id (Entries.ParameterEntry @@ -1831,7 +1831,7 @@ let add_morphism_infer glob m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind ctx instance hook; + Lemmas.start_proof instance_id kind evd instance hook; ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism glob binders m s n = |