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.

5 files changed, 7 insertions, 6 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6a0f4d852..dbd89019e 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -247,7 +247,7 @@ module Btauto = struct
           let fr = reify env fr in
           let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
           Tacticals.New.tclTHENLIST [
-            Proofview.V82.tactic (Tactics.change_in_concl None changed_gl);
+            Proofview.V82.tactic (Tactics.change_concl changed_gl);
             Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
             Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
             try_unification env
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 1f6ece602..7c134da7a 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -587,7 +587,7 @@ let rec fourier gl=
                       else tac_zero_infeq_false gl (rational_to_fraction cres)
            in
            tac:=(tclTHENS (my_cut ineq)
-                     [tclTHEN (change_in_concl None
+                     [tclTHEN (change_concl
 			       (mkAppL [| get coq_not; ineq|]
 				       ))
 		      (tclTHEN (apply (if sres then get coq_Rnot_lt_lt
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f141d3619..38cbd0c53 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -668,7 +668,8 @@ let mkDestructEq :
      [Simple.generalize new_hyps;
       (fun g2 ->
 	change_in_concl None
-	  (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+	  (fun env sigma -> 
+	    sigma, pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
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 |]));
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index c5a0f798c..e22816c13 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1282,7 +1282,7 @@ let resolution env full_reified_goal systems_list =
 
   Tactics.generalize
     (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
-  Tactics.change_in_concl None reified >>
+  Tactics.change_concl reified >>
   Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
   show_goal >>
   Tactics.normalise_vm_in_concl >>