Merge remote-tracking branch 'origin/master' into stm+doc_hook

10 files changed, 38 insertions, 22 deletions

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 523c7c8305..e59076bd63 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -182,9 +182,18 @@ TACTIC EXTEND unify
   }
 END
 
+{
+let deprecated_convert_concl_no_check =
+  CWarnings.create
+    ~name:"convert_concl_no_check" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
+}
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast }
+| ["convert_concl_no_check" constr(x) ] -> {
+    deprecated_convert_concl_no_check ();
+    Tactics.convert_concl ~check:false x DEFAULTcast
+  }
 END
 
 {
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 469551809c..12b12bc7b0 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -278,7 +278,7 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
      }
   | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
-    => { VtUnknown, VtNow }
+    => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
     -> {
           add_morphism_infer atts m n
        }
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index a2dd51643b..c23240b782 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -703,7 +703,11 @@ GRAMMAR EXTEND Gram
       | IDENT "change"; c = conversion; cl = clause_dft_concl ->
 	  { let (oc, c) = c in
 	  let p,cl = merge_occurrences loc cl oc in
-	  TacAtom (CAst.make ~loc @@ TacChange (p,c,cl)) }
+          TacAtom (CAst.make ~loc @@ TacChange (true,p,c,cl)) }
+      | IDENT "change_no_check"; c = conversion; cl = clause_dft_concl ->
+          { let (oc, c) = c in
+          let p,cl = merge_occurrences loc cl oc in
+          TacAtom (CAst.make ~loc @@ TacChange (false,p,c,cl)) }
     ] ]
   ;
 END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 80070a7493..79f0f521cc 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -833,9 +833,10 @@ let pr_goal_selector ~toplevel s =
             pr_red_expr r
             ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
           )
-        | TacChange (op,c,h) ->
+        | TacChange (check,op,c,h) ->
+          let name = if check then "change_no_check" else "change" in
           hov 1 (
-            primitive "change" ++ brk (1,1)
+            primitive name ++ brk (1,1)
             ++ (
               match op with
                   None ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2d40ba6562..963b7189f9 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1574,8 +1574,8 @@ let newfail n s =
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
   (* For compatibility *)
-  let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
-  let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
+  let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
+  let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in
   let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
@@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	    tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
 	| Some id, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
+            convert_hyp ~check:false ~reorder:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
             beta_hyp id
 	| None, Some p ->
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1610,7 +1610,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             end
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_concl_no_check newt DEFAULTcast
+            convert_concl ~check:false newt DEFAULTcast
   in
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
@@ -1800,7 +1800,7 @@ let anew_instance ~pstate atts binders instance fields =
   let program_mode = atts.program in
   new_instance ~pstate ~program_mode atts.polymorphic
     binders instance (Some (true, CAst.make @@ CRecord (fields)))
-    ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info
+    ~global:atts.global ~generalize:false Hints.empty_hint_info
 
 let declare_instance_refl ~pstate atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 30e316b36d..0eb7726a18 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -34,6 +34,7 @@ type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+type check_flag = bool     (* true = check    false = do not check *)
 
 type ('c,'d,'id) inversion_strength =
   | NonDepInversion of
@@ -125,7 +126,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
-  | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+  | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 8b6b14322b..fd303f5d94 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -34,6 +34,7 @@ type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+type check_flag = bool     (* true = check    false = do not check *)
 
 type ('c,'d,'id) inversion_strength =
   | NonDepInversion of
@@ -124,7 +125,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
-  | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+  | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 543d4de0fe..c1f7fab123 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -551,7 +551,7 @@ let rec intern_atomic lf ist x =
   | TacReduce (r,cl) ->
       dump_glob_red_expr r;
       TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
-  | TacChange (None,c,cl) ->
+  | TacChange (check,None,c,cl) ->
       let is_onhyps = match cl.onhyps with
       | None | Some [] -> true
       | _ -> false
@@ -560,17 +560,17 @@ let rec intern_atomic lf ist x =
       | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
       | _ -> false
       in
-      TacChange (None,
+      TacChange (check,None,
         (if is_onhyps && is_onconcl
          then intern_type ist c else intern_constr ist c),
 	clause_app (intern_hyp_location ist) cl)
-  | TacChange (Some p,c,cl) ->
+  | TacChange (check,Some p,c,cl) ->
       let { ltacvars } = ist in
       let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in
       let fold accu x = Id.Set.add x accu in
       let ltacvars = List.fold_left fold ltacvars metas in
       let ist' = { ist with ltacvars } in
-      TacChange (Some pat,intern_constr ist' c,
+      TacChange (check,Some pat,intern_constr ist' c,
 	clause_app (intern_hyp_location ist) cl)
 
   (* Equality and inversion *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 4398fb14ab..800be2565d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1770,7 +1770,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
         (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
       end
-  | TacChange (None,c,cl) ->
+  | TacChange (check,None,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
       Proofview.Goal.enter begin fun gl ->
@@ -1792,10 +1792,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
             then interp_type ist env sigma c
             else interp_constr ist env sigma c
         in
-        Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
+        Tactics.change ~check None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
       end
       end
-  | TacChange (Some op,c,cl) ->
+  | TacChange (check,Some op,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
       Proofview.Goal.enter begin fun gl ->
@@ -1815,7 +1815,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             with e when to_catch e (* Hack *) ->
               user_err  (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
         in
-        Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
+        Tactics.change ~check (Some op) c_interp (interp_clause ist env sigma cl)
       end
       end
 
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index e617f3d45e..a3eeca2267 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -158,8 +158,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
-  | TacChange (op,c,cl) ->
-      TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
+  | TacChange (check,op,c,cl) ->
+      TacChange (check,Option.map (subst_glob_constr_or_pattern subst) op,
         subst_glob_constr subst c, cl)
 
   (* Equality and inversion *)