diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 13:01:31 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 13:10:02 +0200 |
| commit | db37c9f3f32ae7a2abcd5e1a3f6239eddb5e1768 (patch) | |
| tree | 6eaead7c3cd3b61ec54295a9037a4ef568b5dedb /plugins/micromega/coq_micromega.ml | |
| parent | 0b1507b16da38e883d63802db7c013e2c09665fd (diff) | |
Fix semantics of change p with c to typecheck c at each specific occurrence of p,
avoiding unwanted universe constraints in presence of universe polymorphic constants.
Fixing HoTT bugs # 36, 54 and 113.
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d11454b27..ebd042022 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1378,7 +1378,7 @@ let micromega_order_change spec cert cert_typ env ff gl = let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) env in - Tactics.change_in_concl None + Tactics.change_concl (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); @@ -1666,7 +1666,7 @@ let micromega_order_changer cert env ff gl = let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) env in - Tactics.change_in_concl None + Tactics.change_concl (set [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); |