Imported Upstream version 8.6upstream/8.6

8 files changed, 72 insertions, 53 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index ae2d059f..58744b57 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,10 +15,11 @@ open Tacmach
 open Util
 open Declarations
 open Globnames
+open Context.Rel.Declaration
 
 let qflag=ref true
 
-let red_flags=ref Closure.betaiotazeta
+let red_flags=ref CClosure.betaiotazeta
 
 let (=?) f g i1 i2 j1 j2=
   let c=f i1 i2 in
@@ -58,12 +59,12 @@ let ind_hyps nevar ind largs gls=
     Array.map myhyps types
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 type kind_of_formula=
     Arrow of constr*constr
@@ -139,8 +140,8 @@ let build_atoms gl metagen side cciterm =
 		  negative:= unsigned :: !negative
 	    end;
 	  let v = ind_hyps 0 i l gl in
-	  let g i _ (_,_,t) =
-	    build_rec env polarity (lift i t) in
+	  let g i _ decl =
+	    build_rec env polarity (lift i (get_type decl)) in
 	  let f l =
 	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
@@ -150,8 +151,8 @@ let build_atoms gl metagen side cciterm =
       | Exists(i,l)->
 	  let var=mkMeta (metagen true) in
 	  let v =(ind_hyps 1 i l gl).(0) in
-	  let g i _ (_,_,t) =
-	    build_rec (var::env) polarity (lift i t) in
+	  let g i _ decl =
+	    build_rec (var::env) polarity (lift i (get_type decl)) in
 	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
@@ -224,7 +225,7 @@ let build_formula side nam typ gl metagen=
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in
+		      let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 39d99d2e..5db8ff59 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -7,12 +7,11 @@
 (************************************************************************)
 
 open Term
-open Context
 open Globnames
 
 val qflag : bool ref
 
-val red_flags: Closure.RedFlags.reds ref
+val red_flags: CClosure.RedFlags.reds ref
 
 val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
   'a -> 'a -> 'b -> 'b -> int
@@ -27,7 +26,7 @@ type counter = bool -> metavariable
 val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
 
 val ind_hyps : int -> pinductive -> constr list ->
-  Proof_type.goal Tacmach.sigma -> rel_context array
+  Proof_type.goal Tacmach.sigma -> Context.Rel.t array
 
 type atoms = {positive:constr list;negative:constr list}
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 04152688..43fac8ad 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,6 +15,9 @@ open Goptions
 open Tacticals
 open Tacinterp
 open Libnames
+open Constrarg
+open Stdarg
+open Pcoq.Prim
 
 DECLARE PLUGIN "ground_plugin"
 
@@ -52,8 +55,15 @@ let _=
   in
     declare_int_option gdopt
 
+let default_intuition_tac =
+  let tac _ _ = Auto.h_auto None [] None in
+  let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
+  let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
+  Tacenv.register_ml_tactic name [| tac |];
+  Tacexpr.TacML (Loc.ghost, entry, [])
+
 let (set_default_solver, default_solver, print_default_solver) = 
-  Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver"
+  Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
 
 VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
@@ -64,7 +74,7 @@ END
 
 VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
 | [ "Print" "Firstorder" "Solver" ] -> [
-    Pp.msg_info
+    Feedback.msg_info
       (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
 END
 
@@ -106,11 +116,17 @@ open Pp
 open Genarg
 open Ppconstr
 open Printer
-let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
-let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
-let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
+
+let warn_deprecated_syntax =
+  CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
+    (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
+
 
 ARGUMENT EXTEND firstorder_using
+  TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
   RAW_TYPED AS reference_list
   RAW_PRINTED BY pr_firstorder_using_raw
@@ -119,8 +135,7 @@ ARGUMENT EXTEND firstorder_using
 | [ "using" reference(a) ] -> [ [a] ]
 | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
 | [ "using" reference(a) reference(b) reference_list(l) ] -> [
-    Flags.if_verbose
-      Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+    warn_deprecated_syntax ();
     a::b::l
   ]
 | [ ] -> [ [] ]
@@ -128,20 +143,22 @@ END
 
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ]
 |   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ]
 |   [ "firstorder" tactic_opt(t) firstorder_using(l)
        "with" ne_preident_list(l') ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ]
 END
 
 TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
-     [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ]
+     [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ]
 END
 
 open Proofview.Notations
+open Cc_plugin
+open Decl_mode_plugin
 
 let default_declarative_automation =
   Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 3b9f67f6..628af4e7 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -24,15 +24,15 @@ let update_flags ()=
   in
     List.iter f (Classops.coercions ());
     red_flags:=
-    Closure.RedFlags.red_add_transparent
-      Closure.betaiotazeta
+    CClosure.RedFlags.red_add_transparent
+      CClosure.betaiotazeta
       (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
   update_flags ();
   let rec toptac skipped seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
-    then Pp.msg_debug (Printer.pr_goal gl);
+    then Feedback.msg_debug (Printer.pr_goal gl);
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try
diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mlpack
index 447a1fb5..65fb2e9a 100644
--- a/plugins/firstorder/ground_plugin.mllib
+++ b/plugins/firstorder/ground_plugin.mlpack
@@ -5,4 +5,3 @@ Rules
 Instances
 Ground
 G_ground
-Ground_plugin_mod
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a717cc91..eebd974e 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -8,11 +8,10 @@
 
 open Unify
 open Rules
-open Errors
+open CErrors
 open Util
 open Term
 open Vars
-open Glob_term
 open Tacmach
 open Tactics
 open Tacticals
@@ -22,6 +21,8 @@ open Formula
 open Sequent
 open Names
 open Misctypes
+open Sigma.Notations
+open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
 	match inst1,inst2 with
@@ -96,8 +97,6 @@ let rec collect_quantified seq=
 
 (* open instances processor *)
 
-let dummy_constr=mkMeta (-1)
-
 let dummy_bvid=Id.of_string "x"
 
 let mk_open_instance id idc gl m t=
@@ -108,7 +107,7 @@ let mk_open_instance id idc gl m t=
       let typ=pf_unsafe_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
+      let (nam,_,_)=destProd (whd_all env evmap typ) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
@@ -116,8 +115,10 @@ let mk_open_instance id idc gl m t=
   let rec aux n avoid env evmap decls =
     if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id avoid var_id gl) in
-      let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
-      let decl = (Name nid,None,c) in
+      let evmap = Sigma.Unsafe.of_evar_map evmap in
+      let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+      let evmap = Sigma.to_evar_map evmap in
+      let decl = LocalAssum (Name nid, c) in
 	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
     evmap, decls, revt
@@ -134,9 +135,9 @@ let left_instance_tac (inst,id) continue seq=
 	    [tclTHENLIST
 	       [Proofview.V82.of_tactic introf;
                 pf_constr_of_global id (fun idc ->
-		(fun gls->generalize
+		(fun gls-> Proofview.V82.of_tactic (generalize
 		   [mkApp(idc,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
 		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -155,12 +156,12 @@ let left_instance_tac (inst,id) continue seq=
 		      (mkApp(idc,[|ot|])) rc in
 		  let evmap, _ =
 		    try Typing.type_of (pf_env gl) evmap gt
-		    with e when Errors.noncritical e ->
+		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
-		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
+		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
 	    else
 	      pf_constr_of_global id (fun idc ->
-		generalize [mkApp(idc,[|t|])])
+		Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
 	  in
 	    tclTHENLIST
 	      [special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e676a8a9..ffb63af0 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -19,6 +19,7 @@ open Formula
 open Sequent
 open Globnames
 open Locus
+open Context.Named.Declaration
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
@@ -34,12 +35,13 @@ let wrap n b continue seq gls=
     if i<=0 then seq else
       match nc with
 	  []->anomaly (Pp.str "Not the expected number of hyps")
-	| ((id,_,typ) as nd)::q->
+	| nd::q->
+            let id = get_id nd in
 	    if occur_var env id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
+	      add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
   let seq2=if b then
     add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
@@ -50,13 +52,13 @@ let basename_of_global=function
   | _->assert false
 
 let clear_global=function
-    VarRef id->clear [id]
+    VarRef id-> Proofview.V82.of_tactic (clear [id])
   | _->tclIDTAC
 
 (* connection rules *)
 
 let axiom_tac t seq=
-  try pf_constr_of_global (find_left t seq) exact_no_check
+  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq=
@@ -65,7 +67,7 @@ let ll_atom_tac a backtrack id continue seq=
       tclTHENLIST
 	[pf_constr_of_global (find_left a seq) (fun left ->
 	  pf_constr_of_global id (fun id -> 
-	    generalize [mkApp(id, [|left|])]));
+	    Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
 	 clear_global id;
 	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -133,7 +135,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
        let newhyps idc =List.init lp (myterm idc) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
-	      [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
+	      [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
 	       clear_global id;
 	       tclDO lp (Proofview.V82.of_tactic intro)])
 	   (wrap lp false continue seq) backtrack gl
@@ -149,9 +151,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	     clear_global id;
 	     wrap 1 false continue seq];
 	  tclTHENS (Proofview.V82.of_tactic (cut cc))
-            [pf_constr_of_global id exact_no_check;
+            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
 	     tclTHENLIST
-	       [pf_constr_of_global id (fun idc -> generalize [d idc]);
+	       [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
 		clear_global id;
 		Proofview.V82.of_tactic introf;
 		Proofview.V82.of_tactic introf;
@@ -190,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq=
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-		tclTHEN (generalize [term]) (clear [id0]) gls));
+		tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
 	   clear_global id;
 	   Proofview.V82.of_tactic intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
@@ -210,6 +212,6 @@ let defined_connectives=lazy
 let normalize_evaluables=
   onAllHypsAndConcl
     (function
-	 None->unfold_in_concl (Lazy.force defined_connectives)
+	 None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives))
        | Some id ->
-	   unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
+	   Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)))
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 3e8033da..1248b60a 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Term
-open Errors
+open CErrors
 open Util
 open Formula
 open Unify