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.

11 files changed, 52 insertions, 39 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 >>
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 8794557ef..aa32e0e5c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1396,13 +1396,13 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
 	  | Some id, Some p ->
 	      cut_replacing id newt (Tacmach.refine p)
 	  | Some id, None -> 
-	      change_in_hyp None newt (id, InHypTypeOnly)
+	      change_in_hyp None (fun env sigma -> sigma, newt) (id, InHypTypeOnly)
 	  | None, Some p ->
 	      let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
 		tclTHENLAST
 		  (Tacmach.internal_cut false name newt)
 		  (tclTHEN (Proofview.V82.of_tactic (Tactics.revert [name])) (Tacmach.refine p))
-	  | None, None -> change_in_concl None newt
+	  | None, None -> change_in_concl None (fun env sigma -> sigma, newt)
 	in tclTHEN (evartac undef) tac
   in
   let tac =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ca582c82f..97cb50a28 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1710,13 +1710,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
-        let (sigma,c_interp) =
+        let c_interp env sigma =
 	  if is_onhyps && is_onconcl
-	  then pf_interp_type ist gl c
-	  else pf_interp_constr ist gl c
+	  then interp_type ist env sigma c
+	  else interp_constr ist env sigma c
         in
-        tclTHEN
-	  (tclEVARS sigma)
 	  (Tactics.change None c_interp (interp_clause ist (pf_env gl) cl))
           gl
       end
@@ -1728,16 +1726,14 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Proofview.V82.tactic begin fun gl -> 
           let sign,op = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
-	  let env' = Environ.push_named_context sign env in
-          let (sigma',c_interp) =
-	    try interp_constr ist env' sigma c
-	    with e when to_catch e (* Hack *) ->
-	      errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+          let c_interp env sigma =
+	    let env' = Environ.push_named_context sign env in
+	      try interp_constr ist env' sigma c
+	      with e when to_catch e (* Hack *) ->
+		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
           in
-          tclTHEN
-	    (tclEVARS sigma')
-	    (Tactics.change (Some op) c_interp (interp_clause ist env cl))
-            gl
+	      (Tactics.change (Some op) c_interp (interp_clause ist env cl))
+		gl
         end
       end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c7fc4197e..f65f295b2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -345,19 +345,30 @@ let e_reduct_in_hyp redfun (id,where) gl =
     (e_pf_reduce_decl redfun where (pf_get_hyp gl id))
     convert_hyp_no_check gl
 
+type change_arg = env -> evar_map -> evar_map * constr
+
 (* Now we introduce different instances of the previous tacticals *)
 let change_and_check cv_pb t env sigma c =
-  let evd, b = infer_conv ~pb:cv_pb env sigma t c in
-    if b then evd, t
-    else
-      errorlabstrm "convert-check-hyp" (str "Not convertible.")
-
+  let sigma, t' = t env sigma in
+  let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
+    if b then sigma, t'
+    else raise ConstrMatching.PatternMatchingFailure
+
+let change_and_check_subst cv_pb subst t env sigma c =
+  let t' env sigma = 
+    let sigma, t = t env sigma in
+      sigma, replace_vars (Id.Map.bindings subst) t 
+  in change_and_check cv_pb t' env sigma c
+      
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb t = function
-  | None -> change_and_check cv_pb t
+  | None -> fun env sigma c ->
+    (try change_and_check cv_pb t env sigma c
+     with ConstrMatching.PatternMatchingFailure ->
+       errorlabstrm "convert-check-hyp" (str "Not convertible."))
   | Some occl ->
-      e_contextually false occl
-        (fun subst -> change_and_check Reduction.CONV (replace_vars (Id.Map.bindings subst) t))
+    e_contextually false occl
+      (fun subst -> change_and_check_subst Reduction.CONV subst t)
 
 let change_in_concl occl t =
   e_reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
@@ -378,6 +389,9 @@ let change chg c cls gl =
        change_option (bind_change_occurrences occs chg) c None)
     cls gl
 
+let change_concl t = 
+  change_in_concl None (fun env sigma -> sigma, t)
+
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl (red_product,REVERTcast)
 let red_in_hyp          = reduct_in_hyp   red_product
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6574d88c5..5951a4af8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -117,12 +117,14 @@ val exact_proof      : Constrexpr.constr_expr -> tactic
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
+type change_arg = env -> evar_map -> evar_map * constr
+
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
 val reduct_option     : tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
-val change_in_concl   : (occurrences * constr_pattern) option -> constr -> 
-                        tactic
-val change_in_hyp     : (occurrences * constr_pattern) option -> constr ->
+val change_in_concl   : (occurrences * constr_pattern) option -> change_arg -> tactic
+val change_concl      : constr -> tactic
+val change_in_hyp     : (occurrences * constr_pattern) option -> change_arg ->
                         hyp_location -> tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location -> tactic
@@ -144,7 +146,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> tactic
 val change            :
-  constr_pattern option -> constr -> clause -> tactic
+  constr_pattern option -> change_arg -> clause -> tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> tactic
 val reduce            : red_expr -> clause -> tactic
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
index f10856bc7..4c3e078a5 100644
--- a/test-suite/bugs/closed/HoTT_coq_036.v
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -29,8 +29,8 @@ Module Version1.
     assert (Hf : focus ((S tt) = (S tt))) by constructor.
     let C1 := constr:(CObject) in
     let C2 := constr:(fun C => @Object (CObject C) C) in
-    unify C1 C2.
-    progress change CObject with (fun C => @Object (CObject C) C) in *.
+    unify C1 C2; idtac C1 C2. Show Universes.
+    progress change @CObject with (fun C => @Object (CObject C) C) in *. 
     simpl in *.
     match type of Hf with
       | focus ?V => exact V
@@ -112,7 +112,7 @@ Module OtherBug.
 
   Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
                                (objD : Type) (D : SpecializedCategory objD), Prop.
-  Definition CommaCategory_Object (A : Category) : Type.
+  Definition CommaCategory_Object (A : Category@{i}) : Type.
     assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
     progress change CObject with (fun C => @Object (CObject C) C) in *;
       simpl in *.
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
index f79fe1c1e..b47bb3a20 100644
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ b/test-suite/bugs/closed/HoTT_coq_054.v
@@ -47,10 +47,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
                          | inl y' => ap g
                          | inr y' => idmap
                        end
-           | inr x' => match y as y return match y with
+           | inr x' => match y as y return match y return Type with
                                                inr y' => x' = y'
                                              | _ => Empty
-                                           end -> match f y with
+                                           end -> match f y return Type with
                                                     | inr y' => h x' = y'
                                                     | _ => Empty end with
                          | inl y' => idmap