From 9354722485c71ba6fbe6e6462eae98113aa830cc Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 20 Apr 2017 17:50:10 +0200
Subject: Fix nsatz not recognizing real literals.

---
 plugins/nsatz/Nsatz.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'plugins')

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index b11d15e5ca..403f664e2b 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -462,6 +462,11 @@ try (try apply Rsth;
 exact Rplus_opp_r.
 Defined.
 
+Class can_compute_Z (z : Z) := dummy_can_compute_Z : True.
+Hint Extern 0 (can_compute_Z ?v) =>
+  match isZcst v with true => exact I end : typeclass_instances.
+Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z).
+
 Lemma R_one_zero: 1%R <> 0%R.
 discrR.
 Qed.
-- 
cgit v1.2.3


From 804526b13b123c07dd11e1f23f30e8b01c0c8610 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 8 Mar 2017 09:12:41 +0100
Subject: Removing trivial compatibility layer in omega.

---
 plugins/omega/coq_omega.ml | 262 +++++++++++++++++++++++----------------------
 1 file changed, 135 insertions(+), 127 deletions(-)

(limited to 'plugins')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 7780de7127..c57719ac47 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -19,7 +19,7 @@ open Names
 open Nameops
 open Term
 open EConstr
-open Tacticals
+open Tacticals.New
 open Tacmach
 open Tactics
 open Logic
@@ -41,7 +41,9 @@ let elim_id id =
   Proofview.Goal.enter { enter = begin fun gl ->
     simplest_elim (Tacmach.New.pf_global id gl)
   end }
-let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
+let resolve_id id = Proofview.Goal.enter { enter = begin fun gl ->
+  apply (Tacmach.New.pf_global id gl)
+end }
 
 let timing timer_name f arg = f arg
 
@@ -146,7 +148,7 @@ let intern_id,unintern_id,reset_intern_tables =
        Hashtbl.add table v idx; Hashtbl.add co_table idx v; v),
   (fun () -> cpt := 0; Hashtbl.clear table)
 
-let mk_then = tclTHENLIST
+let mk_then tacs = tclTHENLIST tacs
 
 let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
 
@@ -580,9 +582,11 @@ let abstract_path sigma typ path t =
   let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in
   mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
 
-let focused_simpl path gl =
+let focused_simpl path =
+  Proofview.V82.tactic begin fun gl ->
   let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
   Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
+  end
 
 let focused_simpl path = focused_simpl path
 
@@ -642,7 +646,8 @@ let decompile af =
 
 let mkNewMeta () = mkMeta (Evarutil.new_meta())
 
-let clever_rewrite_base_poly typ p result theorem gl =
+let clever_rewrite_base_poly typ p result theorem =
+  Proofview.V82.tactic begin fun gl ->
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
   let t =
@@ -658,12 +663,13 @@ let clever_rewrite_base_poly typ p result theorem gl =
        [abstracted])
   in
   exact (applist(t,[mkNewMeta()])) gl
+  end
 
-let clever_rewrite_base p result theorem gl =
-  clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl
+let clever_rewrite_base p result theorem =
+  clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem
 
-let clever_rewrite_base_nat p result theorem gl =
-  clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem gl
+let clever_rewrite_base_nat p result theorem =
+  clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem
 
 let clever_rewrite_gen p result (t,args) =
   let theorem = applist(t, args) in
@@ -673,12 +679,14 @@ let clever_rewrite_gen_nat p result (t,args) =
   let theorem = applist(t, args) in
   clever_rewrite_base_nat p result theorem
 
-let clever_rewrite p vpath t gl =
+let clever_rewrite p vpath t =
+  Proofview.V82.tactic begin fun gl ->
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
   let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
   exact (applist(t',[mkNewMeta()])) gl
+  end
 
 let rec shuffle p (t1,t2) =
   match t1,t2 with
@@ -942,15 +950,15 @@ let rec transform sigma p t =
 	  transform sigma p
 	    (mkApp (Lazy.force coq_Zplus,
 		     [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
-	Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t
+	unfold sp_Zminus :: tac,t
     | Kapp(Zsucc,[t1]) ->
 	let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer one |])) in
-	Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t
+	unfold sp_Zsucc :: tac,t
     | Kapp(Zpred,[t1]) ->
 	let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer negone |])) in
-	Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t
+	unfold sp_Zpred :: tac,t
    | Kapp(Zmult,[t1;t2]) ->
        let tac1,t1' = transform sigma (P_APP 1 :: p) t1
        and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in
@@ -1068,7 +1076,7 @@ let replay_history tactic_normalisation =
       | HYP e :: l ->
 	  begin
 	    try
-	      Tacticals.New.tclTHEN
+	      tclTHEN
 		(Id.List.assoc (hyp_of_tag e.id) tactic_normalisation)
 		(loop l)
 	    with Not_found -> loop l end
@@ -1080,16 +1088,16 @@ let replay_history tactic_normalisation =
 	  let k = if b then negone else one in
 	  let p_initial = [P_APP 1;P_TYPE] in
 	  let tac= shuffle_mult_right p_initial e1.body k e2.body in
-	  Tacticals.New.tclTHENLIST [
+	  tclTHENLIST [
 	    generalize_tac
 	      [mkApp (Lazy.force coq_OMEGA17, [|
 		val_of eq1;
 		val_of eq2;
 		mk_integer k;
 		mkVar id1; mkVar id2 |])];
-	    Proofview.V82.tactic (mk_then tac);
+	    mk_then tac;
 	    (intros_using [aux]);
-	    Proofview.V82.tactic (resolve_id aux);
+	    resolve_id aux;
             reflexivity
           ]
       | CONTRADICTION (e1,e2) :: l ->
@@ -1104,8 +1112,8 @@ let replay_history tactic_normalisation =
 					Lazy.force coq_Gt;
 					Lazy.force coq_Gt |])
 	    in
-            Tacticals.New.tclTHENS
-	      (Tacticals.New.tclTHENLIST [
+            tclTHENS
+	      (tclTHENLIST [
 		unfold sp_Zle;
 		simpl_in_concl;
 		intro;
@@ -1118,7 +1126,7 @@ let replay_history tactic_normalisation =
 		      mkVar (hyp_of_tag e1.id);
 		      mkVar (hyp_of_tag e2.id) |])
 	  in
-	  Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (generalize_tac [theorem])) (mk_then tac))) (solve_le)
+	  Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le
       | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  let id = hyp_of_tag e1.id in
 	  let eq1 = val_of(decompile e1)
@@ -1128,10 +1136,10 @@ let replay_history tactic_normalisation =
 	  let rhs = mk_plus (mk_times eq2 kk) dd in
 	  let state_eg = mk_eq eq1 rhs in
 	  let tac = scalar_norm_add [P_APP 3] e2.body in
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (cut state_eg)
-	    [ Tacticals.New.tclTHENS
-	        (Tacticals.New.tclTHENLIST [
+	    [ tclTHENS
+	        (tclTHENLIST [
 		  (intros_using [aux]);
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA1,
@@ -1139,9 +1147,9 @@ let replay_history tactic_normalisation =
 		  (clear [aux;id]);
 		  (intros_using [id]);
 		  (cut (mk_gt kk dd)) ])
-	        [ Tacticals.New.tclTHENS
+	        [ tclTHENS
 		    (cut (mk_gt kk izero))
-		    [ Tacticals.New.tclTHENLIST [
+		    [ tclTHENLIST [
 		        (intros_using [aux1; aux2]);
 		        (generalize_tac
 			  [mkApp (Lazy.force coq_Zmult_le_approx,
@@ -1149,13 +1157,13 @@ let replay_history tactic_normalisation =
 		        (clear [aux1;aux2;id]);
 		        (intros_using [id]);
 		        (loop l) ];
-		      Tacticals.New.tclTHENLIST [
+		      tclTHENLIST [
 			(unfold sp_Zgt);
 			simpl_in_concl;
 			reflexivity ] ];
-		  Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
+		  tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
                 ];
-	      Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+	      tclTHEN (mk_then tac) reflexivity ]
 
       | NOT_EXACT_DIVIDE (e1,k) :: l ->
 	  let c = floor_div e1.constant k in
@@ -1166,10 +1174,10 @@ let replay_history tactic_normalisation =
 	  let kk = mk_integer k
 	  and dd = mk_integer d in
 	  let tac = scalar_norm_add [P_APP 2] e2.body in
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (cut (mk_gt dd izero))
-	    [ Tacticals.New.tclTHENS (cut (mk_gt kk dd))
-		[Tacticals.New.tclTHENLIST [
+	    [ tclTHENS (cut (mk_gt kk dd))
+		[tclTHENLIST [
 		  (intros_using [aux2;aux1]);
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_OMEGA4,
@@ -1177,14 +1185,14 @@ let replay_history tactic_normalisation =
 		  (clear [aux1;aux2]);
 		  unfold sp_not;
 		  (intros_using [aux]);
-		  Proofview.V82.tactic (resolve_id aux);
-		  Proofview.V82.tactic (mk_then tac);
+		  resolve_id aux;
+		  mk_then tac;
 		  assumption ] ;
-		 Tacticals.New.tclTHENLIST [
+		 tclTHENLIST [
 		   unfold sp_Zgt;
 		   simpl_in_concl;
 		   reflexivity ] ];
-              Tacticals.New.tclTHENLIST [
+              tclTHENLIST [
 		unfold sp_Zgt;
                 simpl_in_concl;
 		reflexivity ] ]
@@ -1197,9 +1205,9 @@ let replay_history tactic_normalisation =
 	  let state_eq = mk_eq eq1 (mk_times eq2 kk) in
 	  if e1.kind == DISE then
             let tac = scalar_norm [P_APP 3] e2.body in
-            Tacticals.New.tclTHENS
+            tclTHENS
 	      (cut state_eq)
-	      [Tacticals.New.tclTHENLIST [
+	      [tclTHENLIST [
 		(intros_using [aux1]);
 		(generalize_tac
 		  [mkApp (Lazy.force coq_OMEGA18,
@@ -1207,14 +1215,14 @@ let replay_history tactic_normalisation =
 		(clear [aux1;id]);
 		(intros_using [id]);
 		(loop l) ];
-	       Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+	       tclTHEN (mk_then tac) reflexivity ]
 	  else
             let tac = scalar_norm [P_APP 3] e2.body in
-            Tacticals.New.tclTHENS (cut state_eq)
+            tclTHENS (cut state_eq)
 	      [
-		Tacticals.New.tclTHENS
+		tclTHENS
 		 (cut (mk_gt kk izero))
-		 [Tacticals.New.tclTHENLIST [
+		 [tclTHENLIST [
 		   (intros_using [aux2;aux1]);
 		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA3,
@@ -1222,11 +1230,11 @@ let replay_history tactic_normalisation =
 		   (clear [aux1;aux2;id]);
 		   (intros_using [id]);
 		   (loop l) ];
-		  Tacticals.New.tclTHENLIST [
+		  tclTHENLIST [
 		    unfold sp_Zgt;
                     simpl_in_concl;
 		    reflexivity ] ];
-		Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
+		tclTHEN (mk_then tac) reflexivity ]
       | (MERGE_EQ(e3,e1,e2)) :: l ->
 	  let id = new_identifier () in
 	  tag_hypothesis id e3;
@@ -1239,16 +1247,16 @@ let replay_history tactic_normalisation =
 	      (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
             scalar_norm [P_APP 3] e1.body
 	  in
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (cut (mk_eq eq1 (mk_inv eq2)))
-	    [Tacticals.New.tclTHENLIST [
+	    [tclTHENLIST [
 	      (intros_using [aux]);
 	      (generalize_tac [mkApp (Lazy.force coq_OMEGA8,
 	        [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
 	      (clear [id1;id2;aux]);
 	      (intros_using [id]);
 	      (loop l) ];
-            Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity]
+            tclTHEN (mk_then tac) reflexivity]
 
       | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
 	  let id = new_identifier ()
@@ -1272,9 +1280,9 @@ let replay_history tactic_normalisation =
               [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
             shuffle_mult_right p_initial
               orig.body m ({c= negone;v= v}::def.body) in
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (cut theorem)
-	    [Tacticals.New.tclTHENLIST [
+	    [tclTHENLIST [
 	      (intros_using [aux]);
 	      (elim_id aux);
 	      (clear [aux]);
@@ -1282,11 +1290,11 @@ let replay_history tactic_normalisation =
 	      (generalize_tac
 		[mkApp (Lazy.force coq_OMEGA9,
 		  [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
-	      Proofview.V82.tactic (mk_then tac);
+	      mk_then tac;
 	      (clear [aux]);
 	      (intros_using [id]);
 	      (loop l) ];
-            Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ]
+            tclTHEN (exists_tac eq1) reflexivity ]
       | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
 	  let id1 = new_identifier ()
 	  and id2 = new_identifier () in
@@ -1295,10 +1303,10 @@ let replay_history tactic_normalisation =
 	  let tac1 = norm_add [P_APP 2;P_TYPE] e.body in
 	  let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in
 	  let eq = val_of(decompile e) in
-	  Tacticals.New.tclTHENS
+	  tclTHENS
 	    (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
-	    [Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ];
-             Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]]
+	    [tclTHENLIST [ mk_then tac1; (intros_using [id1]); (loop act1) ];
+             tclTHENLIST [ mk_then tac2; (intros_using [id2]); (loop act2) ]]
       | SUM(e3,(k1,e1),(k2,e2)) :: l ->
 	  let id = new_identifier () in
 	  tag_hypothesis id e3;
@@ -1317,10 +1325,10 @@ let replay_history tactic_normalisation =
             let p_initial =
               if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
             let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
-            Tacticals.New.tclTHENLIST [
+            tclTHENLIST [
 	      (generalize_tac
                 [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
-	      Proofview.V82.tactic (mk_then tac);
+	      mk_then tac;
 	      (intros_using [id]);
 	      (loop l)
             ]
@@ -1329,10 +1337,10 @@ let replay_history tactic_normalisation =
 	    and kk2 = mk_integer k2 in
 	    let p_initial = [P_APP 2;P_TYPE] in
 	    let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
-            Tacticals.New.tclTHENS (cut (mk_gt kk1 izero))
-	      [Tacticals.New.tclTHENS
+            tclTHENS (cut (mk_gt kk1 izero))
+	      [tclTHENS
 		 (cut (mk_gt kk2 izero))
-		 [Tacticals.New.tclTHENLIST [
+		 [tclTHENLIST [
 		   (intros_using [aux2;aux1]);
 		   (generalize_tac
 		     [mkApp (Lazy.force coq_OMEGA7, [|
@@ -1340,29 +1348,29 @@ let replay_history tactic_normalisation =
 		       mkVar aux1;mkVar aux2;
 		       mkVar id1;mkVar id2 |])]);
 		   (clear [aux1;aux2]);
-		   Proofview.V82.tactic (mk_then tac);
+		   mk_then tac;
 		   (intros_using [id]);
 		   (loop l) ];
-		 Tacticals.New.tclTHENLIST [
+		 tclTHENLIST [
 		   unfold sp_Zgt;
                    simpl_in_concl;
 		   reflexivity ] ];
-	      Tacticals.New.tclTHENLIST [
+	      tclTHENLIST [
 		unfold sp_Zgt;
                 simpl_in_concl;
 		reflexivity ] ]
       | CONSTANT_NOT_NUL(e,k) :: l ->
-	  Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
+	  tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
       | CONSTANT_NUL(e) :: l ->
-	  Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity
+	  tclTHEN (resolve_id (hyp_of_tag e)) reflexivity
       | CONSTANT_NEG(e,k) :: l ->
-	  Tacticals.New.tclTHENLIST [
+	  tclTHENLIST [
 	    (generalize_tac [mkVar (hyp_of_tag e)]);
             unfold sp_Zle;
 	    simpl_in_concl;
 	    unfold sp_not;
 	    (intros_using [aux]);
-	    Proofview.V82.tactic (resolve_id aux);
+	    resolve_id aux;
 	    reflexivity
           ]
       | _ -> Proofview.tclUNIT ()
@@ -1380,12 +1388,12 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
   let (tac,t') = normalize sigma p_initial t in
   let shift_left =
     tclTHEN
-      (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]))
-      (tclTRY (Proofview.V82.of_tactic (clear [id])))
+      (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
+      (tclTRY (clear [id]))
   in
   if not (List.is_empty tac) then
     let id' = new_identifier () in
-    ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ]))
+    ((id',(tclTHENLIST [ shift_left; mk_then tac; (intros_using [id']) ]))
           :: tactic,
      compile id' flag t' :: defs)
   else
@@ -1430,7 +1438,7 @@ let destructure_omega gl tac_def (id,c) =
 
 let reintroduce id =
   (* [id] cannot be cleared if dependent: protect it by a try *)
-  Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id)
+  tclTHEN (tclTRY (clear [id])) (intro_using id)
 
 
 open Proofview.Notations
@@ -1449,7 +1457,7 @@ let coq_omega =
            let id = new_identifier () in
            let i = new_id () in
            tag_hypothesis id i;
-           (Tacticals.New.tclTHENLIST [
+           (tclTHENLIST [
 	     (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
 	     (intros_using [v; id]);
 	     (elim_id id);
@@ -1460,7 +1468,7 @@ let coq_omega =
 	    body = [{v=intern_id v; c=one}];
             constant = zero; id = i} :: sys
 	 else
-           (Tacticals.New.tclTHENLIST [
+           (tclTHENLIST [
 	     (simplest_elim (applist (Lazy.force coq_new_var, [t])));
 	     (intros_using [v;th]);
 	     tac ]),
@@ -1476,13 +1484,13 @@ let coq_omega =
     with UNSOLVABLE ->
       let _,path = depend [] [] (history ()) in
       if !display_action_flag then display_action display_var path;
-      (Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path))
+      (tclTHEN prelude (replay_history tactic_normalisation path))
   end else begin
     try
       let path = simplify_strong (new_id,new_var_num,display_var) system in
       if !display_action_flag then display_action display_var path;
-      Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)
-    with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system")
+      tclTHEN prelude (replay_history tactic_normalisation path)
+    with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
   end
   end }
 
@@ -1495,36 +1503,36 @@ let nat_inject =
     Proofview.tclEVARMAP >>= fun sigma ->
     try match destructurate_term sigma t with
       | Kapp(Plus,[t1;t2]) ->
-          Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
+          tclTHENLIST [
+	    (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
               ((Lazy.force coq_inj_plus),[t1;t2]));
 	    (explore (P_APP 1 :: p) t1);
 	    (explore (P_APP 2 :: p) t2)
           ]
       | Kapp(Mult,[t1;t2]) ->
-          Tacticals.New.tclTHENLIST [
-	    Proofview.V82.tactic (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
+          tclTHENLIST [
+	    (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
               ((Lazy.force coq_inj_mult),[t1;t2]));
 	    (explore (P_APP 1 :: p) t1);
 	    (explore (P_APP 2 :: p) t2)
           ]
       | Kapp(Minus,[t1;t2]) ->
           let id = new_identifier () in
-          Tacticals.New.tclTHENS
-            (Tacticals.New.tclTHEN
+          tclTHENS
+            (tclTHEN
 	       (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
 	       (intros_using [id]))
 	    [
-	      Tacticals.New.tclTHENLIST [
-	        Proofview.V82.tactic (clever_rewrite_gen p
+	      tclTHENLIST [
+	        (clever_rewrite_gen p
 		  (mk_minus (mk_inj t1) (mk_inj t2))
                   ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id]));
 		(loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]);
 		(explore (P_APP 1 :: p) t1);
 		(explore (P_APP 2 :: p) t2) ];
-	      (Tacticals.New.tclTHEN
-		 (Proofview.V82.tactic (clever_rewrite_gen p (mk_integer zero)
-                    ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])))
+	      (tclTHEN
+		 (clever_rewrite_gen p (mk_integer zero)
+                    ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
 		 (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
 	    ]
       | Kapp(S,[t']) ->
@@ -1538,24 +1546,24 @@ let nat_inject =
           let rec loop p t : unit Proofview.tactic =
             try match destructurate_term sigma t with
 		Kapp(S,[t]) ->
-                  (Tacticals.New.tclTHEN
-                     (Proofview.V82.tactic (clever_rewrite_gen p
+                  (tclTHEN
+                     (clever_rewrite_gen p
 			(mkApp (Lazy.force coq_Zsucc, [| mk_inj t |]))
-			((Lazy.force coq_inj_S),[t])))
+			((Lazy.force coq_inj_S),[t]))
 		     (loop (P_APP 1 :: p) t))
               | _ -> explore p t
             with e when catchable_exception e -> explore p t
 	  in
-          if is_number t' then Proofview.V82.tactic (focused_simpl p) else loop p t
+          if is_number t' then focused_simpl p else loop p t
       | Kapp(Pred,[t]) ->
           let t_minus_one =
 	    mkApp (Lazy.force coq_minus, [| t;
 		      mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
-          Tacticals.New.tclTHEN
-            (Proofview.V82.tactic (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
-               ((Lazy.force coq_pred_of_minus),[t])))
+          tclTHEN
+            (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
+               ((Lazy.force coq_pred_of_minus),[t]))
             (explore p t_minus_one)
-      | Kapp(O,[]) -> Proofview.V82.tactic (focused_simpl p)
+      | Kapp(O,[]) -> focused_simpl p
       | _ -> Proofview.tclUNIT ()
     with e when catchable_exception e -> Proofview.tclUNIT ()
 
@@ -1565,7 +1573,7 @@ let nat_inject =
         Proofview.tclEVARMAP >>= fun sigma ->
 	  begin try match destructurate_prop sigma t with
               Kapp(Le,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1574,7 +1582,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Lt,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1583,7 +1591,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Ge,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1592,7 +1600,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Gt,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
                     [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1601,7 +1609,7 @@ let nat_inject =
 		  (loop lit)
                 ]
             | Kapp(Neq,[t1;t2]) ->
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac
 		    [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
@@ -1611,7 +1619,7 @@ let nat_inject =
                 ]
             | Kapp(Eq,[typ;t1;t2]) ->
 		if is_conv typ (Lazy.force coq_nat) then
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
 		    (explore [P_APP 2; P_TYPE] t1);
@@ -1697,20 +1705,20 @@ let fresh_id avoid id gl =
 let onClearedName id tac =
   (* We cannot ensure that hyps can be cleared (because of dependencies), *)
   (* so renaming may be necessary *)
-  Tacticals.New.tclTHEN
-    (Tacticals.New.tclTRY (clear [id]))
-    (Proofview.Goal.enter { enter = begin fun gl ->
+  tclTHEN
+    (tclTRY (clear [id]))
+    (Proofview.Goal.nf_enter { enter = begin fun gl ->
      let id = fresh_id [] id gl in
-     Tacticals.New.tclTHEN (introduction id) (tac id)
+     tclTHEN (introduction id) (tac id)
     end })
 
 let onClearedName2 id tac =
-  Tacticals.New.tclTHEN
-    (Tacticals.New.tclTRY (clear [id]))
-    (Proofview.Goal.enter { enter = begin fun gl ->
+  tclTHEN
+    (tclTRY (clear [id]))
+    (Proofview.Goal.nf_enter { enter = begin fun gl ->
      let id1 = fresh_id [] (add_suffix id "_left") gl in
      let id2 = fresh_id [] (add_suffix id "_right") gl in
-      Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
+      tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
     end })
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
@@ -1724,7 +1732,7 @@ let destructure_hyps =
   let decidability = decidability gl in
   let pf_nf = pf_nf gl in
     let rec loop = function
-      | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
+      | [] -> (tclTHEN nat_inject coq_omega)
       | decl::lit ->
           let i = NamedDecl.get_id decl in
           Proofview.tclEVARMAP >>= fun sigma ->
@@ -1732,17 +1740,17 @@ let destructure_hyps =
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->
-              (Tacticals.New.tclTHENS
+              (tclTHENS
                  (elim_id i)
                  [ onClearedName i (fun i -> (loop (LocalAssum (i,t1)::lit)));
                    onClearedName i (fun i -> (loop (LocalAssum (i,t2)::lit))) ])
           | Kapp(And,[t1;t2]) ->
-              Tacticals.New.tclTHEN
+              tclTHEN
 		(elim_id i)
 		(onClearedName2 i (fun i1 i2 ->
 		  loop (LocalAssum (i1,t1) :: LocalAssum (i2,t2) :: lit)))
           | Kapp(Iff,[t1;t2]) ->
-	      Tacticals.New.tclTHEN
+	      tclTHEN
 		(elim_id i)
 		(onClearedName2 i (fun i1 i2 ->
 		  loop (LocalAssum (i1,mkArrow t1 t2) :: LocalAssum (i2,mkArrow t2 t1) :: lit)))
@@ -1752,7 +1760,7 @@ let destructure_hyps =
               if is_Prop sigma (type_of t2)
               then
 		let d1 = decidability t1 in
-		Tacticals.New.tclTHENLIST [
+		tclTHENLIST [
 		  (generalize_tac [mkApp (Lazy.force coq_imp_simp,
                                                                [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
@@ -1763,7 +1771,7 @@ let destructure_hyps =
           | Kapp(Not,[t]) ->
               begin match destructurate_prop sigma t with
 		Kapp(Or,[t1;t2]) ->
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
                                             [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
 		    (onClearedName i (fun i ->
@@ -1771,7 +1779,7 @@ let destructure_hyps =
                   ]
 	      | Kapp(And,[t1;t2]) ->
 		  let d1 = decidability t1 in
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_and,
 				                    [| t1; t2; d1; mkVar i |])]);
@@ -1781,7 +1789,7 @@ let destructure_hyps =
 	      | Kapp(Iff,[t1;t2]) ->
 		  let d1 = decidability t1 in
 		  let d2 = decidability t2 in
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_iff,
 				                    [| t1; t2; d1; d2; mkVar i |])]);
@@ -1793,7 +1801,7 @@ let destructure_hyps =
 		    (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
 		       For t1, being decidable implies being Prop. *)
 		  let d1 = decidability t1 in
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 		                            [mkApp (Lazy.force coq_not_imp,
 				                    [| t1; t2; d1; mkVar i |])]);
@@ -1802,7 +1810,7 @@ let destructure_hyps =
                   ]
 	      | Kapp(Not,[t]) ->
 		  let d = decidability t in
-                  Tacticals.New.tclTHENLIST [
+                  tclTHENLIST [
 		    (generalize_tac
 			                    [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
 		    (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit))))
@@ -1810,7 +1818,7 @@ let destructure_hyps =
 	      | Kapp(op,[t1;t2]) ->
 		  (try
 		     let thm = not_binop op in
-                     Tacticals.New.tclTHENLIST [
+                     tclTHENLIST [
 		       (generalize_tac
 			                       [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
 		       (onClearedName i (fun _ -> loop lit))
@@ -1820,14 +1828,14 @@ let destructure_hyps =
                   if !old_style_flag then begin
 		    match destructurate_type sigma (pf_nf typ) with
 		    | Kapp(Nat,_) ->
-                        Tacticals.New.tclTHENLIST [
+                        tclTHENLIST [
 			  (simplest_elim
 			     (mkApp
                                 (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
 			  (onClearedName i (fun _ -> loop lit))
                         ]
 		    | Kapp(Z,_) ->
-                        Tacticals.New.tclTHENLIST [
+                        tclTHENLIST [
 			  (simplest_elim
 			     (mkApp
 				(Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
@@ -1837,12 +1845,12 @@ let destructure_hyps =
                   end else begin
 		    match destructurate_type sigma (pf_nf typ) with
 		    | Kapp(Nat,_) ->
-                        (Tacticals.New.tclTHEN
+                        (tclTHEN
 			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
                                                                      decl))
 			   (loop lit))
 		    | Kapp(Z,_) ->
-                        (Tacticals.New.tclTHEN
+                        (tclTHEN
 			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
                                                                      decl))
 			   (loop lit))
@@ -1870,23 +1878,23 @@ let destructure_goal =
       Proofview.V82.wrap_exceptions prop >>= fun prop ->
       match prop with
       | Kapp(Not,[t]) ->
-          (Tacticals.New.tclTHEN
-	     (Tacticals.New.tclTHEN (unfold sp_not) intro)
+          (tclTHEN
+	     (tclTHEN (unfold sp_not) intro)
 	     destructure_hyps)
-      | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b))
+      | Kimp(a,b) -> (tclTHEN intro (loop b))
       | Kapp(False,[]) -> destructure_hyps
       | _ ->
 	  let goal_tac =
 	    try
 	      let dec = decidability t in
-	      Tacticals.New.tclTHEN
+	      tclTHEN
                 (Proofview.V82.tactic (Tacmach.refine
 		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
 	        intro
 	    with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
 	    | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 	  in
-	  Tacticals.New.tclTHEN goal_tac destructure_hyps
+	  tclTHEN goal_tac destructure_hyps
     in
     (loop concl)
   end }
-- 
cgit v1.2.3


From 0cc7ed04a6a6db666da08a724df3998c1e4888f9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 8 Mar 2017 10:12:01 +0100
Subject: Porting omega to the new tactic API.

---
 plugins/omega/coq_omega.ml | 55 ++++++++++++++++++++++++++++++++++------------
 1 file changed, 41 insertions(+), 14 deletions(-)

(limited to 'plugins')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index c57719ac47..92b092ffe9 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -20,7 +20,7 @@ open Nameops
 open Term
 open EConstr
 open Tacticals.New
-open Tacmach
+open Tacmach.New
 open Tactics
 open Logic
 open Libnames
@@ -154,8 +154,8 @@ let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
 
 let generalize_tac t = generalize t
 let elim t = simplest_elim t
-let exact t = Tacmach.refine t
 let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
+let pf_nf gl c = pf_apply Tacred.simpl gl c
 
 let rev_assoc k =
   let rec loop = function
@@ -583,10 +583,11 @@ let abstract_path sigma typ path t =
   mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
 
 let focused_simpl path =
-  Proofview.V82.tactic begin fun gl ->
+  let open Tacmach.New in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
-  Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
-  end
+  convert_concl_no_check newc DEFAULTcast
+  end }
 
 let focused_simpl path = focused_simpl path
 
@@ -644,12 +645,19 @@ let decompile af =
   in
   loop af.body
 
-let mkNewMeta () = mkMeta (Evarutil.new_meta())
+(** Backward compat to emulate the old Refine: normalize the goal conclusion *)
+let new_hole env sigma c =
+  let c = Reductionops.nf_betaiota (Sigma.to_evar_map sigma) c in
+  Evarutil.new_evar env sigma c
 
 let clever_rewrite_base_poly typ p result theorem =
-  Proofview.V82.tactic begin fun gl ->
+  let open Tacmach.New in
+  let open Sigma in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let full = pf_concl gl in
+  let env = pf_env gl in
   let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
+  Refine.refine { run = begin fun sigma ->
   let t =
     applist
       (mkLambda
@@ -662,8 +670,11 @@ let clever_rewrite_base_poly typ p result theorem =
 		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
        [abstracted])
   in
-  exact (applist(t,[mkNewMeta()])) gl
-  end
+  let argt = mkApp (abstracted, [|result|]) in
+  let Sigma (hole, sigma, p) = new_hole env sigma argt in
+  Sigma (applist (t, [hole]), sigma, p)
+  end }
+  end }
 
 let clever_rewrite_base p result theorem =
   clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem
@@ -679,14 +690,29 @@ let clever_rewrite_gen_nat p result (t,args) =
   let theorem = applist(t, args) in
   clever_rewrite_base_nat p result theorem
 
+(** Solve using the term the term [t _] *)
+let refine_app gl t =
+  let open Tacmach.New in
+  let open Sigma in
+  Refine.refine { run = begin fun sigma ->
+  let env = pf_env gl in
+  let ht = match EConstr.kind (Sigma.to_evar_map sigma) (pf_get_type_of gl t) with
+  | Prod (_, t, _) -> t
+  | _ -> assert false
+  in
+  let Sigma (hole, sigma, p) = new_hole env sigma ht in
+  Sigma (applist (t, [hole]), sigma, p)
+  end }
+
 let clever_rewrite p vpath t =
-  Proofview.V82.tactic begin fun gl ->
+  let open Tacmach.New in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
   let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
-  exact (applist(t',[mkNewMeta()])) gl
-  end
+  refine_app gl t'
+  end }
 
 let rec shuffle p (t1,t2) =
   match t1,t2 with
@@ -1888,8 +1914,9 @@ let destructure_goal =
 	    try
 	      let dec = decidability t in
 	      tclTHEN
-                (Proofview.V82.tactic (Tacmach.refine
-		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
+                (Proofview.Goal.nf_enter { enter = begin fun gl ->
+		                         refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
+		                         end })
 	        intro
 	    with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
 	    | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-- 
cgit v1.2.3


From 1ef92c718ece547826f4c7e5c1ce78a6965e1ca6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 29 Mar 2017 23:16:06 +0200
Subject: Removing trivial compatibility layer in refl_omega.

---
 plugins/romega/const_omega.ml  |  6 ++++--
 plugins/romega/const_omega.mli |  2 +-
 plugins/romega/g_romega.ml4    |  2 +-
 plugins/romega/refl_omega.ml   | 29 +++++++++++++++--------------
 4 files changed, 21 insertions(+), 18 deletions(-)

(limited to 'plugins')

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 5c68078d7d..8d7ae51fc0 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -285,7 +285,7 @@ module type Int = sig
 
   val mk : Bigint.bigint -> Term.constr
   val parse_term : Term.constr -> parse_term
-  val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+  val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
   val is_scalar : Term.constr -> bool
 end
@@ -350,10 +350,12 @@ let parse_term t =
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
 
+let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
+
 let parse_rel gl t =
   try match destructurate t with
     | Kapp("eq",[typ;t1;t2])
-      when destructurate (EConstr.Unsafe.to_constr (Tacmach.pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2)
+      when destructurate (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2)
     | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
     | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
     | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index af50ea0fff..ee7ff451a9 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -168,7 +168,7 @@ module type Int =
     (* parsing a term (one level, except if a number is found) *)
     val parse_term : Term.constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+    val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
     val is_scalar : Term.constr -> bool
   end
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 9a54ad7789..df7e5cb99e 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -38,7 +38,7 @@ let romega_tactic l =
           we'd better leave as little as possible in the conclusion,
           for an easier decidability argument. *)
        (Tactics.intros)
-       (Proofview.V82.tactic total_reflexive_omega_tactic))
+       (total_reflexive_omega_tactic))
 
 
 TACTIC EXTEND romega
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index cfe14b230c..a20589fb46 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Util
+open Proofview.Notations
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -16,13 +17,12 @@ open OmegaSolver
 (* Especially useful debugging functions *)
 let debug = ref false
 
-let show_goal gl =
-  if !debug then (); Tacticals.tclIDTAC gl
+let show_goal = Tacticals.New.tclIDTAC
 
 let pp i = print_int i; print_newline (); flush stdout
 
 (* More readable than the prefix notation *)
-let (>>) = Tacticals.tclTHEN
+let (>>) = Tacticals.New.tclTHEN
 
 let mkApp = Term.mkApp
 
@@ -739,7 +739,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
 (* Destructuration des hypothèses et de la conclusion *)
 
 let reify_gl env gl =
-  let concl = Tacmach.pf_concl gl in
+  let concl = Tacmach.New.pf_concl gl in
   let concl = EConstr.Unsafe.to_constr concl in
   let t_concl =
     Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
@@ -760,7 +760,7 @@ let reify_gl env gl =
     | [] ->
 	if !debug then print_env_reification env;
 	[] in
-  let t_lhyps = loop (Tacmach.pf_hyps_types gl) in
+  let t_lhyps = loop (Tacmach.New.pf_hyps_types gl) in
   (id_concl,t_concl) :: t_lhyps
 
 let rec destructurate_pos_hyp orig list_equations list_depends = function
@@ -1283,21 +1283,22 @@ let resolution env full_reified_goal systems_list =
     CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
   let decompose_tactic = decompose_tree env context solution_tree in
 
-  Proofview.V82.of_tactic (Tactics.generalize
-    (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps))) >>
-  Proofview.V82.of_tactic (Tactics.change_concl reified) >>
-  Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|]))) >>
+  Tactics.generalize
+    (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps)) >>
+  Tactics.change_concl reified >>
+  Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
-  Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >>
+  Tactics.normalise_vm_in_concl >>
   (*i Alternatives to the previous line:
    - Normalisation without VM:
       Tactics.normalise_in_concl
    - Skip the conversion check and rely directly on the QED:
       Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
   i*)
-  Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (Lazy.force coq_I)))
+  Tactics.apply (EConstr.of_constr (Lazy.force coq_I))
 
-let total_reflexive_omega_tactic gl =
+let total_reflexive_omega_tactic =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
   rst_omega_var ();
@@ -1306,9 +1307,9 @@ let total_reflexive_omega_tactic gl =
   let full_reified_goal = reify_gl env gl in
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
-  resolution env full_reified_goal systems_list gl
+  resolution env full_reified_goal systems_list
   with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
-
+  end }
 
 (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
 
-- 
cgit v1.2.3


From d272cd02ef9ba2509c266f58ee39f51106ae53c2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Apr 2017 14:27:24 +0200
Subject: Fix the API of the new pf_constr_of_global.

The current implementation was still using continuation passing-style, and
furthermore was triggering a focus on the goals. We take advantage of the
tactic features instead.
---
 plugins/cc/cctac.ml         | 6 +++---
 plugins/firstorder/rules.ml | 9 +++++----
 plugins/fourier/fourierR.ml | 4 ++--
 3 files changed, 10 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2d9dec095a..b2c609dcbc 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -245,7 +245,7 @@ let app_global f args k =
   Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_app_global f args k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
+  Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args))
 
 let new_refine c = Proofview.V82.tactic (refine c)
 let refine c = refine c
@@ -492,7 +492,7 @@ let congruence_tac depth l =
 *)
 
 let mk_eq f c1 c2 k =
-  Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
+  Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
@@ -501,7 +501,7 @@ let mk_eq f c1 c2 k =
     let evm, _ =  type_of (pf_env gl) evm term in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
-    end })
+    end }
 
 let f_equal =
   Proofview.Goal.enter { enter = begin fun gl ->
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index a60fd4d8f1..96601f74a2 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -14,6 +14,7 @@ open Vars
 open Tacmach
 open Tactics
 open Tacticals
+open Proofview.Notations
 open Termops
 open Formula
 open Sequent
@@ -96,7 +97,7 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
+      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim);
        clear_global id;
        tclDO n (Proofview.V82.of_tactic intro)])
      (wrap n false continue seq)
@@ -110,12 +111,12 @@ let left_or_tac ind backtrack id continue seq gls=
        tclDO n (Proofview.V82.of_tactic intro);
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
+  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim)
 
 (* left arrow connective rules *)
 
@@ -183,7 +184,7 @@ let forall_tac backtrack continue seq=
 let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in
     tclIFTHENELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim))
       (tclTHENLIST [clear_global id;
                     tclDO n (Proofview.V82.of_tactic intro);
                     (wrap (n-1) false continue seq)])
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index e11cbc279a..25d8f8c832 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -617,9 +617,9 @@ let rec fourier () =
       			        [Tacticals.New.tclORELSE
                                    (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
                                    (Proofview.tclUNIT ());
-				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq ->
+				 Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq ->
 					  (Tacticals.New.tclTHEN (apply symeq)
-						(apply (get coq_Rinv_1))))]
+						(apply (get coq_Rinv_1)))]
 
 					 )
 				]));
-- 
cgit v1.2.3


From 91ff75cf42ebc883e2cfcdc4928154315984beb8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Apr 2017 14:51:56 +0200
Subject: Removing tactic compatibility layer in Micromega.

---
 plugins/micromega/coq_micromega.ml | 57 ++++++++++++++++++--------------------
 1 file changed, 27 insertions(+), 30 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 4b87e6e2ed..eb26c5431d 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -901,16 +901,13 @@ struct
    coq_Qeq, Mc.OpEq
   ]
 
-  let has_typ gl t1 typ = 
-   let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in
-   EConstr.eq_constr (Tacmach.project gl) ty typ
-
+  type gl = { env : Environ.env; sigma : Evd.evar_map }
 
   let is_convertible gl t1 t2 = 
-   Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2
+   Reductionops.is_conv gl.env gl.sigma t1 t2
 
   let parse_zop gl (op,args) =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
     match EConstr.kind sigma op with
     | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
     | Ind((n,0),_) ->
@@ -920,7 +917,7 @@ struct
     |   _ -> failwith "parse_zop"
 
   let parse_rop gl (op,args) =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
     match EConstr.kind sigma op with
      | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
      | Ind((n,0),_) ->
@@ -930,7 +927,7 @@ struct
     |   _ -> failwith "parse_zop"
 
   let parse_qop gl (op,args) =
-    (assoc_const (Tacmach.project gl) op qop_table, args.(0) , args.(1))
+    (assoc_const gl.sigma op qop_table, args.(0) , args.(1))
 
   let is_constant sigma t = (* This is an approx *)
    match EConstr.kind sigma t with
@@ -1154,7 +1151,7 @@ struct
    rop_spec
 
   let  parse_arith parse_op parse_expr env cstr gl =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
    if debug
    then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
    match EConstr.kind sigma cstr with
@@ -1199,7 +1196,7 @@ struct
     *)
   
   let parse_formula gl parse_atom env tg term =
-    let sigma = Tacmach.project gl in
+    let sigma = gl.sigma in
 
     let parse_atom env tg t =
       try
@@ -1208,7 +1205,7 @@ struct
       with e when CErrors.noncritical e -> (X(t),env,tg) in
 
     let is_prop term =
-      let sort  = Retyping.get_sort_of (Tacmach.pf_env gl)  (Tacmach.project gl) term in 
+      let sort  = Retyping.get_sort_of gl.env gl.sigma term in 
      Sorts.is_prop sort in
      
     let rec xparse_formula env tg term =
@@ -1720,7 +1717,6 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
  let vm = dump_varmap (spec.typ) (vm_of_list env) in
  (* todo : directly generate the proof term - or generalize before conversion? *)
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-   let gl = Tacmach.New.of_old (fun x -> x) gl in
    Tacticals.New.tclTHENLIST
     [
      Tactics.change_concl
@@ -1730,7 +1726,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
        ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
        ("__wit", cert, cert_typ)
       ]
-      (Tacmach.pf_concl gl))
+      (Tacmach.New.pf_concl gl))
   ] 
   end }
 
@@ -1967,11 +1963,13 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
     Some (ids,ff',res')
 
 
-
 (**
   * Parse the proof environment, and call micromega_tauto
   *)
 
+let fresh_id avoid id gl =
+  Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
 let micromega_gen
     parse_arith 
     (negate:'cst atom -> 'cst mc_cnf)
@@ -1979,17 +1977,17 @@ let micromega_gen
     unsat deduce 
     spec dumpexpr prover tac =
  Proofview.Goal.nf_enter { enter = begin fun gl -> 
-    let gl = Tacmach.New.of_old (fun x -> x) gl in
-    let sigma = Tacmach.project gl in
-    let concl = Tacmach.pf_concl gl in
-    let hyps  = Tacmach.pf_hyps_types gl in
+    let sigma = Tacmach.New.project gl in
+    let concl = Tacmach.New.pf_concl gl in
+    let hyps  = Tacmach.New.pf_hyps_types gl in
     try
-     let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+     let gl0 = { env = Tacmach.New.pf_env gl; sigma } in
+     let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in
      let env = Env.elements env in
      let spec = Lazy.force spec in
      let dumpexpr = Lazy.force dumpexpr in
      
-     match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl with
+     match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl0 with
      | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
      | Some (ids,ff',res') -> 
        let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in
@@ -1998,7 +1996,7 @@ let micromega_gen
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
-       let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+       let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
 
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
@@ -2057,7 +2055,6 @@ let micromega_order_changer cert env ff  =
   let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
   let vm = dump_varmap (typ) (vm_of_list env) in
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-    let gl = Tacmach.New.of_old (fun x -> x) gl in
     Tacticals.New.tclTHENLIST
      [
      (Tactics.change_concl
@@ -2069,7 +2066,7 @@ let micromega_order_changer cert env ff  =
 	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"), [|typ|]));
          ("__wit", cert, cert_typ)
         ]
-        (Tacmach.pf_concl gl)));
+        (Tacmach.New.pf_concl gl)));
      (*      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
      ]
   end }
@@ -2088,20 +2085,20 @@ let micromega_genr prover tac =
     dump_proof = dump_psatz coq_Q dump_q
   } in
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-     let gl = Tacmach.New.of_old (fun x -> x) gl in
-     let sigma = Tacmach.project gl in
-     let concl = Tacmach.pf_concl gl in
-     let hyps  = Tacmach.pf_hyps_types gl in
+     let sigma = Tacmach.New.project gl in
+     let concl = Tacmach.New.pf_concl gl in
+     let hyps  = Tacmach.New.pf_hyps_types gl in
 
      try
-      let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+      let gl0 = { env = Tacmach.New.pf_env gl; sigma } in
+      let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in
        let env = Env.elements env in
        let spec = Lazy.force spec in
        
        let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in
        let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in
        
-       match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl with
+       match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl0 with
        | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") 
        | Some (ids,ff',res') -> 
          let (ff,ids) = formula_hyps_concl 
@@ -2114,7 +2111,7 @@ let micromega_genr prover tac =
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
        let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
-       let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+       let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in 
        
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
-- 
cgit v1.2.3


From 02f8a5fc7d445ee093bc80663646cfea0a915e6d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Apr 2017 17:36:35 +0200
Subject: Removing tactic compatibility layer in congruence.

---
 plugins/cc/cctac.ml  | 128 ++++++++++++++++++++++++++++++---------------------
 plugins/cc/cctac.mli |   2 +-
 2 files changed, 76 insertions(+), 54 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b2c609dcbc..00b31cccee 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -239,21 +239,43 @@ let build_projection intype (cstr:pconstructor) special default gls=
 
 (* generate an adhoc tactic following the proof tree  *)
 
-let _M =mkMeta
-
 let app_global f args k =
-  Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
-
-let new_app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args))
 
-let new_refine c = Proofview.V82.tactic (refine c)
-let refine c = refine c
+let rec gen_holes env sigma t n accu =
+  let open Sigma in
+  if Int.equal n 0 then (sigma, List.rev accu)
+  else match EConstr.kind sigma t with
+  | Prod (_, u, t) ->
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma u in
+    let sigma = Sigma.to_evar_map sigma in
+    let t = EConstr.Vars.subst1 ev t in
+    gen_holes env sigma t (pred n) (ev :: accu)
+  | _ -> assert false
+
+let app_global_with_holes f args n =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
+    let env = Proofview.Goal.env gl in
+    let concl = Proofview.Goal.concl gl in
+    Refine.refine { Sigma.run = begin fun sigma ->
+      let sigma = Sigma.to_evar_map sigma in
+      let t = Tacmach.New.pf_get_type_of gl fc in
+      let t = Termops.prod_applist sigma t (Array.to_list args) in
+      let ans = mkApp (fc, args) in
+      let (sigma, holes) = gen_holes env sigma t n [] in
+      let ans = applist (ans, holes) in
+      let evdref = ref sigma in
+      let () = Typing.e_check env evdref ans concl in
+      Sigma.Unsafe.of_pair (ans, !evdref)
+    end }
+  end }
 
 let assert_before n c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
-      Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
+    Sigma.Unsafe.of_pair (assert_before n c, evm)
   end }
 
 let refresh_type env evm ty =
@@ -281,18 +303,18 @@ let rec proof_tac p : unit Proofview.tactic =
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
 	refresh_universes (type_of l) (fun typ ->
-        new_app_global _sym_eq [|typ;r;l;c|] exact_check)
+        app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
 	let lr = constr_of_term t in
 	refresh_universes (type_of lr) (fun typ ->
-        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check)
+        app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
 	refresh_universes (type_of t2) (fun typ ->
-	let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
-          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)])
+	let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
+          Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)])
     | Congr (p1,p2)->
 	let tf1=constr_of_term p1.p_lhs
 	and tx1=constr_of_term p2.p_lhs
@@ -303,18 +325,18 @@ let rec proof_tac p : unit Proofview.tactic =
 	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
         let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
-	let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
+	let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
+	let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
 	let prf =
-	  app_global _trans_eq
+	  app_global_with_holes _trans_eq
 		[|typfx;
 		  mkApp(tf1,[|tx1|]);
 		  mkApp(tf2,[|tx1|]);
-		  mkApp(tf2,[|tx2|]);_M 2;_M 3|] in
-	  Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine))
-	    [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1);
+		  mkApp(tf2,[|tx2|])|] 2 in
+	  Tacticals.New.tclTHENS prf
+	    [Tacticals.New.tclTHEN lemma1 (proof_tac p1);
   	     Tacticals.New.tclFIRST
-	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
+	       [Tacticals.New.tclTHEN lemma2 (proof_tac p2);
 		reflexivity;
                 Tacticals.New.tclZEROMSG
 		    (Pp.str
@@ -330,8 +352,8 @@ let rec proof_tac p : unit Proofview.tactic =
            build_projection intype cstr special default gl
          in
 	 let injt=
-           app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
-	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)))
+           app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
+	   Tacticals.New.tclTHEN injt (proof_tac prf)))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end }
 
@@ -341,27 +363,29 @@ let refute_tac c t1 t2 p =
   let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
   let k intype =
-    let neweq= new_app_global _eq [|intype;tt1;tt2|] in
+    let neweq= app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
   in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
   end }
 
-let refine_exact_check c gl =
-  let evm, _ = pf_apply type_of gl c in
-    Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
+let refine_exact_check c =
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    let evm, _ = Tacmach.New.pf_apply type_of gl c in
+    Sigma.Unsafe.of_pair (exact_check c, evm)
+  end }
 
 let convert_to_goal_tac c t1 t2 p = 
   Proofview.Goal.enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let k sort =
-    let neweq= new_app_global _eq [|sort;tt1;tt2|] in
+    let neweq= app_global _eq [|sort;tt1;tt2|] in
     let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
     let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
     let identity=mkLambda (Name x,sort,mkRel 1) in
-    let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+    let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
-			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+			   [proof_tac p; endt refine_exact_check]
   in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end }
 
@@ -392,27 +416,25 @@ let discriminate_tac (cstr,u as cstru) p =
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
     let proj = build_projection intype cstru trivial concl gl in
-    let injt=app_global _f_equal
+    let injt = app_global _f_equal
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
             app_global _eq_rect
 		       [|outtype;trivial;pred;identity;concl;injt|] k) in
-    let neweq=new_app_global _eq [|intype;t1;t2|] in
+    let neweq = app_global _eq [|intype;t1;t2|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
 			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
-      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
+      [proof_tac p; endt refine_exact_check])
   end }
 
 (* wrap everything *)
 
-let build_term_to_complete uf meta pac =
+let build_term_to_complete uf pac =
   let cinfo = get_constructor_info uf pac.cnode in
-  let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
-  let dummy_args = List.rev (List.init pac.arity meta) in
-  let all_args = List.rev_append real_args dummy_args in
+  let real_args = List.rev_map (fun i -> constr_of_term (term uf i)) pac.args in
   let (kn, u) = cinfo.ci_constr in
-    applist (mkConstructU (kn, EInstance.make u), all_args)
+  (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity)
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -434,16 +456,17 @@ let cc_tactic depth additionnal_terms =
 	    let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
 	    discriminate_tac cstr p
 	| Incomplete ->
+            let open Glob_term in
             let env = Proofview.Goal.env gl in
-	    let metacnt = ref 0 in
-	    let newmeta _ = incr metacnt; _M !metacnt in
-	    let terms_to_complete =
-	      List.map
-		(build_term_to_complete uf newmeta)
-		(epsilons uf) in
+            let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+            let hole = GHole (Loc.ghost, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
+            let pr_missing (c, missing) =
+              let c = Detyping.detype ~lax:true false [] env sigma c in
+              let holes = List.init missing (fun _ -> hole) in
+              Printer.pr_glob_constr_env env (GApp (Loc.ghost, c, holes))
+            in
 	    Feedback.msg_info
-	      (Pp.str "Goal is solvable by congruence but \
- some arguments are missing.");
+	      (Pp.str "Goal is solvable by congruence but some arguments are missing.");
 	    Feedback.msg_info
 	      (Pp.str "  Try " ++
 		 hov 8
@@ -451,7 +474,7 @@ let cc_tactic depth additionnal_terms =
 		   str "\"congruence with (" ++
 		     prlist_with_sep
 		     (fun () -> str ")" ++ spc () ++ str "(")
-		     (Termops.print_constr_env env sigma)
+		     pr_missing
 		     terms_to_complete ++
 		     str ")\","
 		 end ++
@@ -472,13 +495,13 @@ let cc_tactic depth additionnal_terms =
 		convert_to_hyp_tac ida ta idb tb p
   end }
 
-let cc_fail gls =
-  user_err ~hdr:"Congruence" (Pp.str "congruence failed.")
+let cc_fail =
+  Tacticals.New.tclZEROMSG (Pp.str "congruence failed.")
 
 let congruence_tac depth l =
   Tacticals.New.tclORELSE
     (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l))
-    (Proofview.V82.tactic cc_fail)
+    cc_fail
 
 (* Beware: reflexivity = constructor 1 = apply refl_equal
    might be slow now, let's rather do something equivalent
@@ -493,14 +516,13 @@ let congruence_tac depth l =
 
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
     let evm, _ =  type_of (pf_env gl) evm term in
-    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
-			  (k term)
+    Sigma.Unsafe.of_pair (k term, evm)
     end }
 
 let f_equal =
@@ -511,7 +533,7 @@ let f_equal =
       try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
 	  (mk_eq _eq c1 c2 Tactics.cut)
-	  [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)]
+	  [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index de6eb982ee..5099d847b0 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -14,7 +14,7 @@ val proof_tac: Ccproof.proof -> unit Proofview.tactic
 
 val cc_tactic : int -> constr list ->  unit Proofview.tactic
 
-val cc_fail : tactic
+val cc_fail : unit Proofview.tactic
 
 val congruence_tac : int -> constr list -> unit Proofview.tactic
 
-- 
cgit v1.2.3


From a1fd5fb489237a1300adb242e2c9b6c74c82981b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Apr 2017 14:16:04 +0200
Subject: Porting the firstorder plugin to the new tactic API.

---
 plugins/firstorder/formula.ml    | 105 ++++++++++++------------
 plugins/firstorder/formula.mli   |  13 +--
 plugins/firstorder/g_ground.ml4  |  39 +++++----
 plugins/firstorder/ground.ml     |  38 +++++----
 plugins/firstorder/ground.mli    |   4 +-
 plugins/firstorder/instances.ml  | 112 ++++++++++++++------------
 plugins/firstorder/instances.mli |   4 +-
 plugins/firstorder/rules.ml      | 169 ++++++++++++++++++++++-----------------
 plugins/firstorder/rules.mli     |   3 +
 plugins/firstorder/sequent.ml    |  61 +++++++-------
 plugins/firstorder/sequent.mli   |  30 +++----
 plugins/firstorder/unify.ml      |  58 +++++++-------
 plugins/firstorder/unify.mli     |   7 +-
 13 files changed, 346 insertions(+), 297 deletions(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 7773f6a2fd..ade94e98e3 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -9,6 +9,7 @@
 open Hipattern
 open Names
 open Term
+open EConstr
 open Vars
 open Termops
 open Tacmach
@@ -44,28 +45,27 @@ let rec nb_prod_after n c=
 	1+(nb_prod_after 0 b)
     | _ -> 0
 
-let construct_nhyps ind gls =
+let construct_nhyps env ind =
   let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in
-  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
+  let constr_types = Inductiveops.arities_of_constructors env ind in
   let hyp = nb_prod_after nparams in
     Array.map hyp constr_types
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
-let ind_hyps nevar ind largs gls=
-  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
+let ind_hyps env sigma nevar ind largs =
+  let types= Inductiveops.arities_of_constructors env ind in
   let myhyps t =
-    let t1=Term.prod_applist t largs in
-    let t2=snd (decompose_prod_n_assum nevar t1) in
-      fst (decompose_prod_assum t2) in
+    let t = EConstr.of_constr t in
+    let t1=Termops.prod_applist sigma t largs in
+    let t2=snd (decompose_prod_n_assum sigma nevar t1) in
+      fst (decompose_prod_assum sigma t2) in
     Array.map myhyps types
 
-let special_nf gl=
-  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> CClosure.norm_val infos (CClosure.inject t))
+let special_nf env sigma t =
+  Reductionops.clos_norm_flags !red_flags env sigma t
 
-let special_whd gl=
-  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let special_whd env sigma t =
+  Reductionops.clos_whd_flags !red_flags env sigma t
 
 type kind_of_formula=
     Arrow of constr*constr
@@ -78,20 +78,19 @@ type kind_of_formula=
 
 let pop t = Vars.lift (-1) t
 
-let kind_of_formula gl term =
-  let normalize=special_nf gl in
-  let cciterm=special_whd gl term in
-    match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with
-	Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b)))
+let kind_of_formula env sigma term =
+  let normalize = special_nf env sigma in
+  let cciterm = special_whd env sigma term in
+    match match_with_imp_term sigma cciterm with
+	Some (a,b)-> Arrow (a, pop b)
       |_->
-	 match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with
-	     Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b)
+	 match match_with_forall_term sigma cciterm with
+	     Some (_,a,b)-> Forall (a, b)
 	   |_->
-	      match match_with_nodep_ind (project gl) (EConstr.of_constr cciterm) with
+	      match match_with_nodep_ind sigma cciterm with
 		  Some (i,l,n)->
-                    let l = List.map EConstr.Unsafe.to_constr l in
-		    let ind,u=EConstr.destInd (project gl) i in
-		    let u = EConstr.EInstance.kind (project gl) u in
+		    let ind,u=EConstr.destInd sigma i in
+		    let u = EConstr.EInstance.kind sigma u in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
 		      if Int.equal nconstr 0 then
@@ -100,7 +99,7 @@ let kind_of_formula gl term =
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in
+			    Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
 			    Array.exists is_constant mip.mind_nf_lc in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
@@ -112,11 +111,11 @@ let kind_of_formula gl term =
 			    else
 			      Or((ind,u),l,is_trivial)
 		| _ ->
-		    match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with
+		    match match_with_sigma_type sigma cciterm with
 			Some (i,l)->
-                          let (ind, u) = EConstr.destInd (project gl) i in
-                          let u = EConstr.EInstance.kind (project gl) u in
-                          Exists((ind, u), List.map EConstr.Unsafe.to_constr l)
+                          let (ind, u) = EConstr.destInd sigma i in
+                          let u = EConstr.EInstance.kind sigma u in
+                          Exists((ind, u), l)
 		      |_-> Atom (normalize cciterm)
 
 type atoms = {positive:constr list;negative:constr list}
@@ -127,29 +126,29 @@ let no_atoms = (false,{positive=[];negative=[]})
 
 let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *)
 
-let build_atoms gl metagen side cciterm =
+let build_atoms env sigma metagen side cciterm =
   let trivial =ref false
   and positive=ref []
   and negative=ref [] in
-  let normalize=special_nf gl in
-  let rec build_rec env polarity cciterm=
-    match kind_of_formula gl cciterm with
+  let normalize=special_nf env sigma in
+  let rec build_rec subst polarity cciterm=
+    match kind_of_formula env sigma cciterm with
 	False(_,_)->if not polarity then trivial:=true
       | Arrow (a,b)->
-	  build_rec env (not polarity) a;
-	  build_rec env polarity b
+	  build_rec subst (not polarity) a;
+	  build_rec subst polarity b
       | And(i,l,b) | Or(i,l,b)->
 	  if b then
 	    begin
-	      let unsigned=normalize (substnl env 0 cciterm) in
+	      let unsigned=normalize (substnl subst 0 cciterm) in
 		if polarity then
 		  positive:= unsigned :: !positive
 		else
 		  negative:= unsigned :: !negative
 	    end;
-	  let v = ind_hyps 0 i l gl in
+	  let v = ind_hyps env sigma 0 i l in
 	  let g i _ decl =
-	    build_rec env polarity (lift i (RelDecl.get_type decl)) in
+	    build_rec subst polarity (lift i (RelDecl.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 *)
@@ -158,16 +157,16 @@ let build_atoms gl metagen side cciterm =
 	    Array.iter f v
       | Exists(i,l)->
 	  let var=mkMeta (metagen true) in
-	  let v =(ind_hyps 1 i l gl).(0) in
+	  let v =(ind_hyps env sigma 1 i l).(0) in
 	  let g i _ decl =
-	    build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in
+	    build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in
 	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
-	    build_rec (var::env) polarity b
+	    build_rec (var::subst) polarity b
       | Atom t->
-	  let unsigned=substnl env 0 t in
-	    if not (isMeta unsigned) then (* discarding wildcard atoms *)
+	  let unsigned=substnl subst 0 t in
+	    if not (isMeta sigma unsigned) then (* discarding wildcard atoms *)
 	      if polarity then
 		positive:= unsigned :: !positive
 	      else
@@ -177,9 +176,9 @@ let build_atoms gl metagen side cciterm =
 	  Concl    -> build_rec [] true cciterm
 	| Hyp      -> build_rec [] false cciterm
 	| Hint     ->
-	    let rels,head=decompose_prod cciterm in
-	    let env=List.rev_map (fun _->mkMeta (metagen true)) rels in
-	      build_rec env false head;trivial:=false (* special for hints *)
+	    let rels,head=decompose_prod sigma cciterm in
+	    let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in
+	      build_rec subst false head;trivial:=false (* special for hints *)
     end;
     (!trivial,
      {positive= !positive;
@@ -215,32 +214,32 @@ type t={id:global_reference;
 	pat:(left_pattern,right_pattern) sum;
 	atoms:atoms}
 
-let build_formula side nam typ gl metagen=
-  let normalize = special_nf gl in
+let build_formula env sigma side nam typ metagen=
+  let normalize = special_nf env sigma in
     try
       let m=meta_succ(metagen false) in
       let trivial,atoms=
 	if !qflag then
-	  build_atoms gl metagen side typ
+	  build_atoms env sigma metagen side typ
 	else no_atoms in
       let pattern=
 	match side with
 	    Concl ->
 	      let pat=
-		match kind_of_formula gl typ with
+		match kind_of_formula env sigma typ with
 		    False(_,_)        -> Rfalse
 		  | Atom a       -> raise (Is_atom a)
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in
+		      let d = RelDecl.get_type (List.last (ind_hyps env sigma 0 i l).(0)) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
 		Right pat
 	  | _ ->
 	      let pat=
-		match kind_of_formula gl typ with
+		match kind_of_formula env sigma typ with
 		    False(i,_)        ->  Lfalse
 		  | Atom a       ->  raise (Is_atom a)
 		  | And(i,_,b)         ->
@@ -257,7 +256,7 @@ let build_formula side nam typ gl metagen=
 		  | Arrow (a,b) ->
 		      let nfa=normalize a in
 			LA (nfa,
-			    match kind_of_formula gl a with
+			    match kind_of_formula env sigma a with
 				False(i,l)-> LLfalse(i,l)
 			      | Atom t->     LLatom
 			      | And(i,l,_)-> LLand(i,l)
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 5db8ff59ad..3f438c04a0 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open Globnames
 
 val qflag : bool ref
@@ -23,10 +24,10 @@ type ('a,'b) sum = Left of 'a | Right of 'b
 
 type counter = bool -> metavariable
 
-val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
+val construct_nhyps : Environ.env -> pinductive -> int array
 
-val ind_hyps : int -> pinductive -> constr list ->
-  Proof_type.goal Tacmach.sigma -> Context.Rel.t array
+val ind_hyps : Environ.env -> Evd.evar_map -> int -> pinductive ->
+  constr list -> EConstr.rel_context array
 
 type atoms = {positive:constr list;negative:constr list}
 
@@ -34,7 +35,7 @@ type side = Hyp | Concl | Hint
 
 val dummy_id: global_reference
 
-val build_atoms : Proof_type.goal Tacmach.sigma -> counter ->
+val build_atoms : Environ.env -> Evd.evar_map -> counter ->
   side -> constr -> bool * atoms
 
 type right_pattern =
@@ -69,6 +70,6 @@ type t={id: global_reference;
 
 (*exception Is_atom of constr*)
 
-val build_formula : side -> global_reference -> types ->
-  Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum
+val build_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> types ->
+  counter -> (t,types) sum
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 3c03193196..8ef6a09d0e 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -13,7 +13,9 @@ open Formula
 open Sequent
 open Ground
 open Goptions
-open Tacticals
+open Tacmach.New
+open Tacticals.New
+open Proofview.Notations
 open Tacinterp
 open Libnames
 open Stdarg
@@ -81,21 +83,29 @@ END
 
 let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 
-let gen_ground_tac flag taco ids bases gl=
+let gen_ground_tac flag taco ids bases =
   let backup= !qflag in
-    try
+  Proofview.tclOR begin
+  Proofview.Goal.enter { enter = begin fun gl ->
       qflag:=flag;
       let solver=
 	match taco with
 	    Some tac-> tac
 	  | None-> snd (default_solver ()) in
-      let startseq gl=
+      let startseq k =
+        Proofview.Goal.s_enter { s_enter = begin fun gl ->
 	let seq=empty_seq !ground_depth in
-        let seq,gl = extend_with_ref_list ids seq gl in
-        extend_with_auto_hints bases seq gl in
-      let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in
-	qflag:=backup;result
-    with reraise -> qflag:=backup;raise reraise
+        let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
+        let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
+        Sigma.Unsafe.of_pair (k seq, sigma)
+        end }
+      in
+      let result=ground_tac solver startseq in
+      qflag := backup;
+      result
+  end }
+  end
+  (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e)
 
 (* special for compatibility with Intuition
 
@@ -144,18 +154,15 @@ END
 
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ]
+      [ 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 (tactic_of_value ist) t) [] l) ]
+      [ 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 (tactic_of_value ist) t) l l') ]
+      [ 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 (tactic_of_value ist) t) [] []) ]
+     [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ]
 END
-
-open Proofview.Notations
-open Cc_plugin
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index d6cd7e2a08..ab1dd07c11 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -12,8 +12,9 @@ open Sequent
 open Rules
 open Instances
 open Term
-open Tacmach
-open Tacticals
+open Tacmach.New
+open Tacticals.New
+open Proofview.Notations
 
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
@@ -29,18 +30,24 @@ let update_flags ()=
       CClosure.betaiotazeta
       (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
-let ground_tac solver startseq gl=
+let ground_tac solver startseq =
+  Proofview.Goal.enter { enter = begin fun gl ->
   update_flags ();
-  let rec toptac skipped seq gl=
-    if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
-    then Feedback.msg_debug (Printer.pr_goal gl);
+  let rec toptac skipped seq =
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let () =
+      if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
+      then
+        let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in
+        Feedback.msg_debug (Printer.pr_goal gl)
+    in
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try
-	  let (hd,seq1)=take_formula seq
-	  and re_add s=re_add_formula_list skipped s in
+	  let (hd,seq1)=take_formula (project gl) seq
+	  and re_add s=re_add_formula_list (project gl) skipped s in
 	  let continue=toptac []
-	  and backtrack gl=toptac (hd::skipped) seq1 gl in
+	  and backtrack =toptac (hd::skipped) seq1 in
 	    match hd.pat with
 		Right rpat->
 		  begin
@@ -60,7 +67,7 @@ let ground_tac solver startseq gl=
 			  or_tac  backtrack continue (re_add seq1)
 		      | Rfalse->backtrack
 		      | Rexists(i,dom,triv)->
-			  let (lfp,seq2)=collect_quantified seq in
+			  let (lfp,seq2)=collect_quantified (project gl) seq in
 			  let backtrack2=toptac (lfp@skipped) seq2 in
 			    if  !qflag && seq.depth>0 then
 			      quantified_tac lfp backtrack2
@@ -80,7 +87,7 @@ let ground_tac solver startseq gl=
 			  left_or_tac ind backtrack
 			  hd.id continue (re_add seq1)
 		      | Lforall (_,_,_)->
-			  let (lfp,seq2)=collect_quantified seq in
+			  let (lfp,seq2)=collect_quantified (project gl) seq in
 			  let backtrack2=toptac (lfp@skipped) seq2 in
 			    if  !qflag && seq.depth>0 then
 			      quantified_tac lfp backtrack2
@@ -119,7 +126,8 @@ let ground_tac solver startseq gl=
 			    ll_atom_tac typ la_tac hd.id continue (re_add seq1)
 		  end
 	    with Heap.EmptyHeap->solver
-      end gl in
-    let seq, gl' = startseq gl in
-    wrap (List.length (pf_hyps gl)) true (toptac []) seq gl'
-
+      end
+    end } in
+    let n = List.length (Proofview.Goal.hyps gl) in
+    startseq (fun seq -> wrap n true (toptac []) seq)
+  end }
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index b5669463cd..4fd1e38a27 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -6,6 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-val ground_tac:     Tacmach.tactic ->
-  (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic
+val ground_tac: unit Proofview.tactic ->
+  ((Sequent.t -> unit Proofview.tactic) -> unit Proofview.tactic) -> unit Proofview.tactic
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 9dc2a51a61..62f811546d 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -11,10 +11,12 @@ open Rules
 open CErrors
 open Util
 open Term
+open EConstr
 open Vars
-open Tacmach
+open Tacmach.New
 open Tactics
-open Tacticals
+open Tacticals.New
+open Proofview.Notations
 open Termops
 open Reductionops
 open Formula
@@ -25,11 +27,12 @@ open Sigma.Notations
 open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
+        let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
 	match inst1,inst2 with
 	    Phantom(d1),Phantom(d2)->
-	      (OrderedConstr.compare d1 d2)
+	      (cmp d1 d2)
 	  | Real((m1,c1),n1),Real((m2,c2),n2)->
-	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2
+	      ((-) =? (-) ==? cmp) m2 m1 n1 n2 c1 c2
 	  | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1
 	  | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1
 
@@ -56,12 +59,12 @@ let make_simple_atoms seq=
       | None->[]
   in {negative=seq.latoms;positive=ratoms}
 
-let do_sequent setref triv id seq i dom atoms=
+let do_sequent sigma setref triv id seq i dom atoms=
   let flag=ref true in
   let phref=ref triv in
   let do_atoms a1 a2 =
     let do_pair t1 t2 =
-      match unif_atoms i dom t1 t2 with
+      match unif_atoms sigma i dom t1 t2 with
 	  None->()
 	| Some (Phantom _) ->phref:=true
 	| Some c ->flag:=false;setref:=IS.add (c,id) !setref in
@@ -71,26 +74,26 @@ let do_sequent setref triv id seq i dom atoms=
     do_atoms atoms (make_simple_atoms seq);
     !flag && !phref
 
-let match_one_quantified_hyp setref seq lf=
+let match_one_quantified_hyp sigma setref seq lf=
   match lf.pat with
       Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
-	if do_sequent setref triv lf.id seq i dom lf.atoms then
+	if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
 	  setref:=IS.add ((Phantom dom),lf.id) !setref
     | _ -> anomaly (Pp.str "can't happen")
 
-let give_instances lf seq=
+let give_instances sigma lf seq=
   let setref=ref IS.empty in
-    List.iter (match_one_quantified_hyp setref seq) lf;
+    List.iter (match_one_quantified_hyp sigma setref seq) lf;
     IS.elements !setref
 
 (* collector for the engine *)
 
-let rec collect_quantified seq=
+let rec collect_quantified sigma seq=
   try
-    let hd,seq1=take_formula seq in
+    let hd,seq1=take_formula sigma seq in
       (match hd.pat with
 	   Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) ->
-	     let (q,seq2)=collect_quantified seq1 in
+	     let (q,seq2)=collect_quantified sigma seq1 in
 	       ((hd::q),seq2)
 	 | _->[],seq)
   with Heap.EmptyHeap -> [],seq
@@ -99,60 +102,61 @@ let rec collect_quantified seq=
 
 let dummy_bvid=Id.of_string "x"
 
-let mk_open_instance id idc gl m t=
-  let env=pf_env gl in
-  let evmap=Refiner.project gl in
+let mk_open_instance env evmap id idc m t =
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_unsafe_type_of gl idc in
+      let typ=Typing.unsafe_type_of env evmap idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in
+      let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
   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 nid=(fresh_id_in_env avoid var_id env) 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) (EConstr.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
-    evmap, decls, revt
+  (evmap, decls, revt)
 
 (* tactics   *)
 
 let left_instance_tac (inst,id) continue seq=
   let open EConstr in
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let sigma = project gl in
   match inst with
       Phantom dom->
-	if lookup (id,None) seq then
+	if lookup sigma (id,None) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
-	  tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
+	  tclTHENS (cut dom)
 	    [tclTHENLIST
-	       [Proofview.V82.of_tactic introf;
-                pf_constr_of_global id (fun idc ->
-		(fun gls-> Proofview.V82.of_tactic (generalize
-		   [mkApp(idc,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
-		Proofview.V82.of_tactic introf;
+	       [introf;
+                (pf_constr_of_global id >>= fun idc ->
+                Proofview.Goal.enter { enter = begin fun gl ->
+                  let id0 = List.nth (pf_ids_of_hyps gl) 0 in
+                  generalize [mkApp(idc, [|mkVar id0|])]
+                end });
+		introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
-	    tclTRY (Proofview.V82.of_tactic assumption)]
-    | Real((m,t) as c,_)->
-	if lookup (id,Some c) seq then
+	    tclTRY assumption]
+    | Real((m,t),_)->
+        let c = (m, EConstr.to_constr sigma t) in
+	if lookup sigma (id,Some c) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
 	  let special_generalize=
 	    if m>0 then
-	      pf_constr_of_global id (fun idc ->
-		fun gl->
-		  let evmap,rc,ot = mk_open_instance id idc gl m t in
-		  let ot = EConstr.of_constr ot in
+	      (pf_constr_of_global id >>= fun idc ->
+		Proofview.Goal.s_enter { s_enter = begin fun gl->
+		  let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
@@ -160,34 +164,38 @@ let left_instance_tac (inst,id) continue seq=
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
-		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
+		    Sigma.Unsafe.of_pair (generalize [gt], evmap)
+                end })
 	    else
-              let t = EConstr.of_constr t in
-	      pf_constr_of_global id (fun idc ->
-		Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
+	      pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
 	  in
 	    tclTHENLIST
 	      [special_generalize;
-	       Proofview.V82.of_tactic introf;
+	       introf;
 	       tclSOLVE
 		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
+  end }
 
 let right_instance_tac inst continue seq=
+  let open EConstr in
+  Proofview.Goal.enter { enter = begin fun gl ->
   match inst with
       Phantom dom ->
-	tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
+	tclTHENS (cut dom)
 	[tclTHENLIST
-	   [Proofview.V82.of_tactic introf;
-	    (fun gls->
-	       Proofview.V82.of_tactic (split (ImplicitBindings
-			[EConstr.mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
+	   [introf;
+            Proofview.Goal.enter { enter = begin fun gl ->
+              let id0 = List.nth (pf_ids_of_hyps gl) 0 in
+              split (ImplicitBindings [mkVar id0])
+            end };
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
-	 tclTRY (Proofview.V82.of_tactic assumption)]
+	 tclTRY assumption]
     | Real ((0,t),_) ->
-	(tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr t])))
+	(tclTHEN (split (ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
+  end }
 
 let instance_tac inst=
   if (snd inst)==dummy_id then
@@ -195,10 +203,10 @@ let instance_tac inst=
   else
     left_instance_tac inst
 
-let quantified_tac lf backtrack continue seq gl=
-  let insts=give_instances lf seq in
+let quantified_tac lf backtrack continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let insts=give_instances (project gl) lf seq in
     tclORELSE
       (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
-      backtrack gl
-
-
+      backtrack
+  end }
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index ce711f3f97..47550f314e 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -9,9 +9,9 @@
 open Globnames
 open Rules
 
-val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
+val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t
 
-val give_instances : Formula.t list -> Sequent.t ->
+val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t ->
   (Unify.instance * global_reference) list
 
 val quantified_tac : Formula.t list -> seqtac with_backtracking
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 96601f74a2..e0d2c38a73 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -10,10 +10,11 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Vars
-open Tacmach
+open Tacmach.New
 open Tactics
-open Tacticals
+open Tacticals.New
 open Proofview.Notations
 open Termops
 open Formula
@@ -23,148 +24,165 @@ open Locus
 
 module NamedDecl = Context.Named.Declaration
 
+type tactic = unit Proofview.tactic
+
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
 type lseqtac= global_reference -> seqtac
 
 type 'a with_backtracking = tactic -> 'a
 
-let wrap n b continue seq gls=
+let wrap n b continue seq =
+  Proofview.Goal.nf_enter { enter = begin fun gls ->
   Control.check_for_interrupt ();
-  let nc=pf_hyps gls in
+  let nc = Proofview.Goal.hyps gls in
   let env=pf_env gls in
+  let sigma = project gls in
   let rec aux i nc ctx=
     if i<=0 then seq else
       match nc with
 	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| nd::q->
             let id = NamedDecl.get_id nd in
-	    if occur_var env (project gls) id (pf_concl gls) ||
-	      List.exists (occur_var_in_decl env (project gls)  id) ctx then
+	    if occur_var env sigma id (pf_concl gls) ||
+	      List.exists (occur_var_in_decl env sigma id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (NamedDecl.get_type nd)) (aux (i-1) q (nd::ctx)) gls in
+	      add_formula env sigma Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
   let seq1=aux n nc [] in
   let seq2=if b then
-    add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in
-    continue seq2 gls
+    add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
+    continue seq2
+  end }
 
 let basename_of_global=function
     VarRef id->id
   | _->assert false
 
 let clear_global=function
-    VarRef id-> Proofview.V82.of_tactic (clear [id])
+    VarRef id-> clear [id]
   | _->tclIDTAC
 
 (* connection rules *)
 
-let axiom_tac t seq=
-  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 axiom_tac t seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  try
+    pf_constr_of_global (find_left (project gl) t seq) >>= fun c ->
+    exact_no_check c
+  with Not_found -> tclFAIL 0 (Pp.str "No axiom link")
+  end }
 
-let ll_atom_tac a backtrack id continue seq=
+let ll_atom_tac a backtrack id continue seq =
   let open EConstr in
   tclIFTHENELSE
-    (try
-      tclTHENLIST
-	[pf_constr_of_global (find_left a seq) (fun left ->
-	  pf_constr_of_global id (fun id -> 
-	    Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))])));
+      (tclTHENLIST
+	[(Proofview.tclEVARMAP >>= fun sigma ->
+          let gr =
+            try Proofview.tclUNIT (find_left sigma a seq)
+            with Not_found -> tclFAIL 0 (Pp.str "No link")
+          in
+          gr >>= fun gr ->
+          pf_constr_of_global gr >>= fun left ->
+	  pf_constr_of_global id >>= fun id -> 
+	    generalize [(mkApp(id, [|left|]))]);
 	 clear_global id;
-	 Proofview.V82.of_tactic intro]
-    with Not_found->tclFAIL 0 (Pp.str "No link"))
+	 intro])
     (wrap 1 false continue seq) backtrack
 
 (* right connectives rules *)
 
 let and_tac backtrack continue seq=
-  tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack
+  tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
 
 let or_tac backtrack continue seq=
   tclORELSE
-    (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq))))))
+    (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
     backtrack
 
 let arrow_tac backtrack continue seq=
-  tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq)
+  tclIFTHENELSE intro (wrap 1 true continue seq)
     (tclORELSE
-       (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq)))
+       (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
        backtrack)
 (* left connectives rules *)
 
-let left_and_tac ind backtrack id continue seq gls=
- let n=(construct_nhyps ind gls).(0) in
+let left_and_tac ind backtrack id continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let n=(construct_nhyps (pf_env gl) ind).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim);
+      [(pf_constr_of_global id >>= simplest_elim);
        clear_global id;
-       tclDO n (Proofview.V82.of_tactic intro)])
+       tclDO n intro])
      (wrap n false continue seq)
-     backtrack gls
+     backtrack
+  end }
 
-let left_or_tac ind backtrack id continue seq gls=
-  let v=construct_nhyps ind gls in
+let left_or_tac ind backtrack id continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let v=construct_nhyps (pf_env gl) ind in
   let f n=
     tclTHENLIST
       [clear_global id;
-       tclDO n (Proofview.V82.of_tactic intro);
+       tclDO n intro;
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim))
+      (pf_constr_of_global id >>= simplest_elim)
       (Array.map f v)
-      backtrack gls
+      backtrack
+  end }
 
 let left_false_tac id=
-  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim)
+  Tacticals.New.pf_constr_of_global id >>= simplest_elim
 
 (* left arrow connective rules *)
 
 (* We use this function for false, and, or, exists *)
 
-let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
-     let rcs=ind_hyps 0 indu largs gl in
+let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+     let rcs=ind_hyps (pf_env gl) (project gl) 0 indu largs in
      let vargs=Array.of_list largs in
              (* construire le terme  H->B, le generaliser etc *)
      let myterm idc i=
        let rc=rcs.(i) in
        let p=List.length rc in
+       let u = EInstance.make u in
        let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
        let head=mkApp ((lift p idc),[|capply|]) in
-         EConstr.of_constr (it_mkLambda_or_LetIn head rc) in
+         EConstr.it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
-       let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in
+       let newhyps idc =List.init lp (myterm idc) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
-	      [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
+	      [(pf_constr_of_global id >>= fun idc -> generalize (newhyps idc));
 	       clear_global id;
-	       tclDO lp (Proofview.V82.of_tactic intro)])
-	   (wrap lp false continue seq) backtrack gl
+	       tclDO lp intro])
+	   (wrap lp false continue seq) backtrack
+  end }
 
 let ll_arrow_tac a b c backtrack id continue seq=
   let open EConstr in
   let open Vars in
-  let a = EConstr.of_constr a in
-  let b = EConstr.of_constr b in
-  let c = EConstr.of_constr c in
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
   let d idc = mkLambda (Anonymous,b,
 		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
-      (tclTHENS (Proofview.V82.of_tactic (cut c))
+      (tclTHENS (cut c)
 	 [tclTHENLIST
-	    [Proofview.V82.of_tactic introf;
+	    [introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
-	  tclTHENS (Proofview.V82.of_tactic (cut cc))
-            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
+	  tclTHENS (cut cc)
+            [(pf_constr_of_global id >>= fun c -> exact_no_check c);
 	     tclTHENLIST
-	       [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
+	       [(pf_constr_of_global id >>= fun idc -> generalize [d idc]);
 		clear_global id;
-		Proofview.V82.of_tactic introf;
-		Proofview.V82.of_tactic introf;
+		introf;
+		introf;
 		tclCOMPLETE (wrap 2 true continue seq)]]])
       backtrack
 
@@ -172,38 +190,40 @@ let ll_arrow_tac a b c backtrack id continue seq=
 
 let forall_tac backtrack continue seq=
   tclORELSE
-    (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq)
+    (tclIFTHENELSE intro (wrap 0 true continue seq)
        (tclORELSE
-	  (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq)))
+	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
 	  backtrack))
     (if !qflag then
        tclFAIL 0 (Pp.str "reversible in 1st order mode")
      else
        backtrack)
 
-let left_exists_tac ind backtrack id continue seq gls=
-  let n=(construct_nhyps ind gls).(0) in
+let left_exists_tac ind backtrack id continue seq =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let n=(construct_nhyps (pf_env gl) ind).(0) in
     tclIFTHENELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id >>= simplest_elim))
+      (Tacticals.New.pf_constr_of_global id >>= simplest_elim)
       (tclTHENLIST [clear_global id;
-                    tclDO n (Proofview.V82.of_tactic intro);
+                    tclDO n intro;
                     (wrap (n-1) false continue seq)])
       backtrack
-      gls
+  end }
 
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
-    (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr prod)))
+    (tclTHENS (cut prod)
        [tclTHENLIST
-	  [Proofview.V82.of_tactic intro;
-           pf_constr_of_global id (fun idc ->
-	   (fun gls->
+	  [intro;
+           (pf_constr_of_global id >>= fun idc ->
+	   Proofview.Goal.enter { enter = begin fun gls->
               let open EConstr in
-	      let id0=pf_nth_hyp_id gls 1 in
+	      let id0 = List.nth (pf_ids_of_hyps gls) 0 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-		tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
+              tclTHEN (generalize [term]) (clear [id0])
+           end });
 	   clear_global id;
-	   Proofview.V82.of_tactic intro;
+	   intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
 	tclCOMPLETE (wrap 0 true continue (deepen seq))])
     backtrack
@@ -215,12 +235,13 @@ let ll_forall_tac prod backtrack id continue seq=
 let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [AllOccurrences,EvalConstRef (fst (destConst (constant "not")));
-   AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))]
+  [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not")));
+   AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))]
 
 let normalize_evaluables=
-  onAllHypsAndConcl
-    (function
-	 None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives))
-       | Some id ->
-	   Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)))
+  Proofview.Goal.enter { enter = begin fun gl ->
+    unfold_in_concl (Lazy.force defined_connectives) <*>
+    tclMAP
+      (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
+      (pf_ids_of_hyps gl)
+  end }
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 381b7cd87c..80a7ae2c25 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -7,10 +7,13 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open Tacmach
 open Names
 open Globnames
 
+type tactic = unit Proofview.tactic
+
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
 type lseqtac= global_reference -> seqtac
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index fb0c22c2b7..59b842c825 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open CErrors
 open Util
 open Formula
@@ -57,11 +58,11 @@ end
 
 module OrderedConstr=
 struct
-  type t=constr
+  type t=Constr.t
   let compare=constr_ord
 end
 
-type h_item = global_reference * (int*constr) option
+type h_item = global_reference * (int*Constr.t) option
 
 module Hitem=
 struct
@@ -81,13 +82,15 @@ module CM=Map.Make(OrderedConstr)
 
 module History=Set.Make(Hitem)
 
-let cm_add typ nam cm=
+let cm_add sigma typ nam cm=
+  let typ = EConstr.to_constr sigma typ in
   try
     let l=CM.find typ cm in CM.add typ (nam::l) cm
   with
       Not_found->CM.add typ [nam] cm
 
-let cm_remove typ nam cm=
+let cm_remove sigma typ nam cm=
+  let typ = EConstr.to_constr sigma typ in
   try
     let l=CM.find typ cm in
     let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
@@ -112,19 +115,19 @@ let deepen seq={seq with depth=seq.depth-1}
 
 let record item seq={seq with history=History.add item seq.history}
 
-let lookup item seq=
+let lookup sigma item seq=
   History.mem item seq.history ||
   match item with
       (_,None)->false
-    | (id,Some ((m,t) as c))->
+    | (id,Some (m, t))->
 	let p (id2,o)=
 	  match o with
 	      None -> false
-	    | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in
+	    | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
 	  History.exists p seq.history
 
-let add_formula side nam t seq gl=
-  match build_formula side nam t gl seq.cnt with
+let add_formula env sigma side nam t seq =
+  match build_formula env sigma side nam t seq.cnt with
       Left f->
 	begin
 	  match side with
@@ -136,7 +139,7 @@ let add_formula side nam t seq gl=
 	    | _ ->
 		{seq with
 		   redexes=HP.add f seq.redexes;
-		   context=cm_add f.constr nam seq.context}
+		   context=cm_add sigma f.constr nam seq.context}
 	end
     | Right t->
 	match side with
@@ -144,18 +147,18 @@ let add_formula side nam t seq gl=
 	      {seq with gl=t;glatom=Some t}
 	  | _ ->
 	      {seq with
-		 context=cm_add t nam seq.context;
+		 context=cm_add sigma t nam seq.context;
 		 latoms=t::seq.latoms}
 
-let re_add_formula_list lf seq=
+let re_add_formula_list sigma lf seq=
   let do_one f cm=
     if f.id == dummy_id then cm
-    else cm_add f.constr f.id cm in
+    else cm_add sigma f.constr f.id cm in
   {seq with
      redexes=List.fold_right HP.add lf seq.redexes;
      context=List.fold_right do_one lf seq.context}
 
-let find_left t seq=List.hd (CM.find t seq.context)
+let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context)
 
 (*let rev_left seq=
   try
@@ -164,7 +167,7 @@ let find_left t seq=List.hd (CM.find t seq.context)
   with Heap.EmptyHeap -> false
 *)
 
-let rec take_formula seq=
+let rec take_formula sigma seq=
   let hd=HP.maximum seq.redexes
   and hp=HP.remove seq.redexes in
     if hd.id == dummy_id then
@@ -172,11 +175,11 @@ let rec take_formula seq=
 	if seq.gl==hd.constr then
 	  hd,nseq
 	else
-	  take_formula nseq (* discarding deprecated goal *)
+	  take_formula sigma nseq (* discarding deprecated goal *)
     else
       hd,{seq with
 	    redexes=hp;
-	    context=cm_remove hd.constr hd.id seq.context}
+	    context=cm_remove sigma hd.constr hd.id seq.context}
 
 let empty_seq depth=
   {redexes=HP.empty;
@@ -196,18 +199,17 @@ let expand_constructor_hints =
     | gr ->
 	[gr])
 
-let extend_with_ref_list l seq gl =
+let extend_with_ref_list env sigma l seq =
   let l = expand_constructor_hints l in
-  let f gr (seq,gl) =
-    let gl, c = pf_eapply Evd.fresh_global gl gr in
-    let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
-    let typ = EConstr.Unsafe.to_constr typ in
-      (add_formula Hyp gr typ seq gl,gl) in
-    List.fold_right f l (seq,gl)
+  let f gr (seq, sigma) =
+    let sigma, c = Evd.fresh_global env sigma gr in
+    let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in
+      (add_formula env sigma Hyp gr typ seq, sigma) in
+    List.fold_right f l (seq, sigma)
 
 open Hints
 
-let extend_with_auto_hints l seq gl=
+let extend_with_auto_hints env sigma l seq =
   let seqref=ref seq in
   let f p_a_t =
     match repr_hint p_a_t.code with
@@ -215,10 +217,9 @@ let extend_with_auto_hints l seq gl=
       | Res_pf_THEN_trivial_fail (c,_) ->
           let (c, _, _) = c in
 	  (try
-	     let (gr, _) = Termops.global_of_constr (project gl) c in
-	     let typ=(pf_unsafe_type_of gl c) in
-	     let typ = EConstr.Unsafe.to_constr typ in
-	       seqref:=add_formula Hint gr typ !seqref gl
+	     let (gr, _) = Termops.global_of_constr sigma c in
+	     let typ=(Typing.unsafe_type_of env sigma c) in
+	       seqref:=add_formula env sigma Hint gr typ !seqref
 	   with Not_found->())
       | _-> () in
   let g _ _ l = List.iter f l in
@@ -230,7 +231,7 @@ let extend_with_auto_hints l seq gl=
 	error ("Firstorder: "^dbname^" : No such Hint database") in
       Hint_db.iter g hdb in
     List.iter h l;
-    !seqref, gl (*FIXME: forgetting about universes*)
+    !seqref, sigma (*FIXME: forgetting about universes*)
 
 let print_cmap map=
   let print_entry c l s=
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 06c9251e7b..18d68f54f9 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -7,22 +7,23 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open Formula
 open Tacmach
 open Globnames
 
-module OrderedConstr: Set.OrderedType with type t=constr
+module OrderedConstr: Set.OrderedType with type t=Constr.t
 
-module CM: CSig.MapS with type key=constr
+module CM: CSig.MapS with type key=Constr.t
 
-type h_item = global_reference * (int*constr) option
+type h_item = global_reference * (int*Constr.t) option
 
 module History: Set.S with type elt = h_item
 
-val cm_add : constr -> global_reference -> global_reference list CM.t ->
+val cm_add : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t ->
   global_reference list CM.t
 
-val cm_remove : constr -> global_reference -> global_reference list CM.t ->
+val cm_remove : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t ->
   global_reference list CM.t
 
 module HP: Heap.S with type elt=Formula.t
@@ -40,23 +41,22 @@ val deepen: t -> t
 
 val record: h_item -> t -> t
 
-val lookup: h_item -> t -> bool
+val lookup: Evd.evar_map -> h_item -> t -> bool
 
-val add_formula : side -> global_reference -> constr -> t ->
-  Proof_type.goal sigma -> t
+val add_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> constr -> t -> t
 
-val re_add_formula_list : Formula.t list -> t -> t
+val re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t
 
-val find_left : constr -> t -> global_reference
+val find_left : Evd.evar_map -> constr -> t -> global_reference
 
-val take_formula : t -> Formula.t * t
+val take_formula : Evd.evar_map -> t -> Formula.t * t
 
 val empty_seq : int -> t
 
-val extend_with_ref_list : global_reference list ->
-  t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
+val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list ->
+  t -> t * Evd.evar_map
 
-val extend_with_auto_hints : Hints.hint_db_name list ->
-  t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
+val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list ->
+  t -> t * Evd.evar_map
 
 val print_cmap: global_reference list CM.t -> Pp.std_ppcmds
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 7cbfb8e7de..49bf07155f 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -8,6 +8,7 @@
 
 open Util
 open Term
+open EConstr
 open Vars
 open Termops
 open Reductionops
@@ -21,13 +22,12 @@ exception UFAIL of constr*constr
    to the equation set. Raises UFAIL with a pair of  terms
 *)
 
-let strip_outer_cast t =
-  EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *)
-
 let pop t = Vars.lift (-1) t
+let subst_meta subst t =
+  let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in
+  EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t))
 
-let unif t1 t2=
-  let evd = Evd.empty in (** FIXME *)
+let unif evd t1 t2=
   let bige=Queue.create ()
   and sigma=ref [] in
   let bind i t=
@@ -35,7 +35,7 @@ let unif t1 t2=
       (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in
   let rec head_reduce t=
     (* forbids non-sigma-normal meta in head position*)
-    match kind_of_term t with
+    match EConstr.kind evd t with
 	Meta i->
 	  (try
 	     head_reduce (Int.List.assoc i !sigma)
@@ -44,25 +44,25 @@ let unif t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1)))
-      and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in
-	match (kind_of_term nt1),(kind_of_term nt2) with
+      let nt1=head_reduce (whd_betaiotazeta evd t1)
+      and nt2=head_reduce (whd_betaiotazeta evd t2) in
+	match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with
 	    Meta i,Meta j->
 	      if not (Int.equal i j) then
 		if i<j then bind j nt1
 		else bind i nt2
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
-		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
-		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
+		if Int.Set.is_empty (free_rels evd t) &&
+		  not (occur_term evd (EConstr.mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
-		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
-		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
+		if Int.Set.is_empty (free_rels evd t) &&
+		  not (occur_term evd (EConstr.mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
-	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
- 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
+	  | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
+ 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
 	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
@@ -84,19 +84,19 @@ let unif t1 t2=
 		  for i=0 to l-1 do
 		    Queue.add (va.(i),vb.(i)) bige
 		  done
-	  | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2))
+	  | _->if not (eq_constr_nounivs evd nt1 nt2) then raise (UFAIL (nt1,nt2))
     done;
       assert false
 	(* this place is unreachable but needed for the sake of typing *)
     with Queue.Empty-> !sigma
 
-let value i t=
+let value evd i t=
   let add x y=
     if x<0 then y else if y<0 then x else x+y in
   let rec vaux term=
-    if isMeta term && Int.equal (destMeta term) i then 0 else
+    if isMeta evd term && Int.equal (destMeta evd term) i then 0 else
       let f v t=add v (vaux t) in
-      let vr=fold_constr f (-1) term in
+      let vr=EConstr.fold evd f (-1) term in
 	if vr<0 then -1 else vr+1 in
     vaux t
 
@@ -104,11 +104,11 @@ type instance=
     Real of (int*constr)*int
   | Phantom of constr
 
-let mk_rel_inst t=
+let mk_rel_inst evd t=
   let new_rel=ref 1 in
   let rel_env=ref [] in
   let rec renum_rec d t=
-    match kind_of_term t with
+    match EConstr.kind evd t with
 	Meta n->
 	  (try
 	     mkRel (d+(Int.List.assoc n !rel_env))
@@ -117,15 +117,15 @@ let mk_rel_inst t=
 	       incr new_rel;
 	       rel_env:=(n,m) :: !rel_env;
 	       mkRel (m+d))
-      | _ -> map_constr_with_binders succ renum_rec d t
+      | _ -> EConstr.map_with_binders evd succ renum_rec d t
   in
   let nt=renum_rec 0 t in (!new_rel - 1,nt)
 
-let unif_atoms i dom t1 t2=
+let unif_atoms evd i dom t1 t2=
   try
-    let t=Int.List.assoc i (unif t1 t2) in
-      if isMeta t then Some (Phantom dom)
-      else Some (Real(mk_rel_inst t,value i t1))
+    let t=Int.List.assoc i (unif evd t1 t2) in
+      if isMeta evd t then Some (Phantom dom)
+      else Some (Real(mk_rel_inst evd t,value evd i t1))
   with
       UFAIL(_,_) ->None
     | Not_found ->Some (Phantom dom)
@@ -134,11 +134,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *)
   let l=List.init n (fun i->mkMeta (k+i)) in
     substl l t
 
-let more_general (m1,t1) (m2,t2)=
+let more_general evd (m1,t1) (m2,t2)=
   let mt1=renum_metas_from 0 m1 t1
   and mt2=renum_metas_from m1 m2 t2 in
     try
-      let sigma=unif mt1 mt2 in
-      let p (n,t)= n<m1 || isMeta t in
+      let sigma=unif evd mt1 mt2 in
+      let p (n,t)= n<m1 || isMeta evd t in
 	List.for_all p sigma
     with UFAIL(_,_)->false
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 4fe9ad38d8..c9cca9bd8d 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -7,15 +7,16 @@
 (************************************************************************)
 
 open Term
+open EConstr
 
 exception UFAIL of constr*constr
 
-val unif : constr -> constr -> (int*constr) list
+val unif : Evd.evar_map -> constr -> constr -> (int*constr) list
 
 type instance=
     Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
   | Phantom of constr        (* domaine de quantification *)
 
-val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
+val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option
 
-val more_general : (int*constr) -> (int*constr) -> bool
+val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool
-- 
cgit v1.2.3


From 98da9fdce866728f93bc7cb690275f5559aa9bae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Apr 2017 20:37:15 +0200
Subject: Removing various tactic compatibility layers in core tactics.

---
 plugins/ltac/g_class.ml4   |  2 +-
 plugins/ltac/g_rewrite.ml4 | 13 +++++++++----
 plugins/ltac/rewrite.ml    |  6 +++---
 3 files changed, 13 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 40f30c7943..ff5e7d5ff2 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -85,7 +85,7 @@ TACTIC EXTEND not_evar
 END
 
 TACTIC EXTEND is_ground
-  [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
+  [ "is_ground" constr(ty) ] -> [ is_ground ty ]
 END
 
 TACTIC EXTEND autoapply
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c50100bf55..fdcaedab3a 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -19,6 +19,7 @@ open Geninterp
 open Extraargs
 open Tacmach
 open Tacticals
+open Proofview.Notations
 open Rewrite
 open Stdarg
 open Pcoq.Vernac_
@@ -123,15 +124,19 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
+  Proofview.Goal.enter { enter = begin fun gl ->
   let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in
-    Tacticals.onAllHypsAndConcl
+  let hyps = Tacmach.New.pf_ids_of_hyps gl in
+    Tacticals.New.tclMAP
       (fun cl ->
         match cl with
-          | Some id when is_tac id -> tclIDTAC
-          | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
+          | Some id when is_tac id -> Tacticals.New.tclIDTAC
+          | _ -> cl_rewrite_clause c o AllOccurrences cl)
+      (None :: List.map (fun id -> Some id) hyps)
+  end }
 
 TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
+| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
 END
 
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600c..12a1566e20 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2197,7 +2197,8 @@ let setoid_transitivity c =
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
-  Proofview.V82.tactic (fun gl ->
+  let open Tacmach.New in
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let ctype = pf_unsafe_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum sigma ctype in
@@ -2211,11 +2212,10 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
-   Proofview.V82.of_tactic
     (tclTHENLAST
       (Tactics.assert_after_replacing id new_hyp)
       (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
-      gl)
+  end }
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
-- 
cgit v1.2.3


From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Jun 2016 19:12:49 -0400
Subject: Add transparent_abstract tactic

---
 plugins/ltac/extratactics.ml4 | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..a96623a5f6 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -815,6 +815,19 @@ TACTIC EXTEND destauto
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
+(**********************************************************************)
+
+(**********************************************************************)
+(* A version of abstract constructing transparent terms               *)
+(* Introduced by Jason Gross and Benjamin Delaware in June 2016       *)
+(**********************************************************************)
+
+TACTIC EXTEND transparent_abstract
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ]
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ]
+END
 
 (* ********************************************************************* *)
 
-- 
cgit v1.2.3


From 8a3cd2fe699540f1ae5a56917d0f6b951f81d731 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:29:35 +0200
Subject: Remove unused [rec] keywords

---
 plugins/ltac/pptactic.ml | 4 ++--
 plugins/nsatz/nsatz.ml   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 39ae1f41d2..b73b66e56f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -250,7 +250,7 @@ type 'a extra_genarg_printer =
   let pr_alias_key key =
     try
       let prods = (KNmap.find key !prnotation_tab).pptac_prods in
-      let rec pr = function
+      let pr = function
       | TacTerm s -> primitive s
       | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
       in
@@ -314,7 +314,7 @@ type 'a extra_genarg_printer =
   | Extend.Uentry _ | Extend.Uentryl _ ->
     str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
 
-  let rec pr_targ prtac symb arg = match symb with
+  let pr_targ prtac symb arg = match symb with
   | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
     prtac (1, Any) arg
   | Extend.Uentryl (_, l) -> prtac (l, Any) arg
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index db8f3e4b21..a5b0166116 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -437,7 +437,7 @@ open Ideal
    that has the same size than lp and where true indicates an
    element that has been removed
  *)
-let rec clean_pol lp =
+let clean_pol lp =
   let t = Hashpol.create 12 in
   let find p = try Hashpol.find t p 
                with 
-- 
cgit v1.2.3


From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

---
 plugins/extraction/extract_env.ml   |  2 +-
 plugins/ltac/tacentries.ml          |  2 +-
 plugins/ssrmatching/ssrmatching.ml4 | 18 +++++++++---------
 3 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2b12462ad5..322fbcea74 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -657,7 +657,7 @@ let extraction_library is_rec m =
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,struc) =
     if Visit.needed_mp mp
-    then (mp, extract_structure env mp no_delta true struc) :: l
+    then (mp, extract_structure env mp no_delta ~all:true struc) :: l
     else l
   in
   let struc = List.fold_left select [] l in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index cd8c9e471e..8cda73b4bf 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -320,7 +320,7 @@ let add_tactic_notation local n prods e =
   let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map interp_prod_item prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local n prods false ids tac
+  add_glob_tactic_notation local ~level:n prods false ids tac
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index f3555ebc4c..fc7963b2d3 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1261,7 +1261,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let occ = match pattern with Some (_, T _) -> occ | _ -> noindex in
     let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in
     let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in
-    let concl = find_T env0 concl0 1 do_subst in
+    let concl = find_T env0 concl0 1 ~k:do_subst in
     let _ = end_T () in
     concl
   | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) ->
@@ -1273,11 +1273,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     (* we start from sigma, so hole is considered a rigid head *)
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in
-    let concl = find_T env0 concl0 1 (fun env c _ h ->
+    let concl = find_T env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
       fs p_sigma (find_X env (fs sigma p) h 
-        (fun env _ -> do_subst env e_body))) in
+        ~k:(fun env _ -> do_subst env e_body))) in
     let _ = end_X () in let _ = end_T () in 
     concl
   | Some (sigma, E_In_X_In_T (e, hole, p)) ->
@@ -1289,11 +1289,11 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_X, end_X = mk_tpattern_matcher sigma noindex holep in
     let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in
     let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in
-    let concl = find_T env0 concl0 1 (fun env c _ h ->
+    let concl = find_T env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
-        find_E env e_body h do_subst))) in
+      fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h ->
+        find_E env e_body h ~k:do_subst))) in
     let _ = end_E () in let _ = end_X () in let _ = end_T () in
     concl
   | Some (sigma, E_As_X_In_T (e, hole, p)) ->
@@ -1306,10 +1306,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in
     let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in
     let find_X, end_X = mk_tpattern_matcher sigma occ holep in
-    let concl = find_TE env0 concl0 1 (fun env c _ h ->
+    let concl = find_TE env0 concl0 1 ~k:(fun env c _ h ->
       let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in
       let sigma, e_body = pop_evar p_sigma ex p in
-      fs p_sigma (find_X env (fs sigma p) h (fun env c _ h ->
+      fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h ->
         let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in
         let e_body = fs e_sigma e in
         do_subst env e_body e_body h))) in
@@ -1352,7 +1352,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
  let ise, u = mk_tpattern env sigma0 (ise,EConstr.Unsafe.to_constr t) ok L2R p in
  let find_U, end_U =
    mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in
- let concl = find_U env concl h (fun _ _ _ -> mkRel) in
+ let concl = find_U env concl h ~k:(fun _ _ _ -> mkRel) in
  let rdx, _, (sigma, uc, p) = end_U () in
  sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx
 
-- 
cgit v1.2.3


From a5f33b5fda592c2dfaed0c16d3773b35e7acab28 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:52:33 +0200
Subject: Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum

---
 plugins/micromega/mfourier.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index f4f9b3c2f1..3779944154 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -99,7 +99,7 @@ module PSet = ISet
 module System = Hashtbl.Make(Vect)
 
 type proof =
-| Hyp of int
+| Assum of int
 | Elim of  var * proof * proof
 | And of proof * proof
 
@@ -134,7 +134,7 @@ exception SystemContradiction of proof
 let hyps prf =
   let rec hyps prf acc =
     match prf with
-      | Hyp i -> ISet.add i acc
+      | Assum i -> ISet.add i acc
       | Elim(_,prf1,prf2)
       | And(prf1,prf2) -> hyps prf1 (hyps prf2 acc) in
     hyps prf ISet.empty
@@ -143,7 +143,7 @@ let hyps prf =
 (** Pretty printing *)
   let rec pp_proof o prf =
     match prf with
-      | Hyp i -> Printf.fprintf o "H%i" i
+      | Assum i -> Printf.fprintf o "H%i" i
       | Elim(v, prf1,prf2) -> Printf.fprintf o "E(%i,%a,%a)" v pp_proof prf1 pp_proof prf2
       | And(prf1,prf2)   -> Printf.fprintf o "A(%a,%a)"  pp_proof prf1 pp_proof prf2
 
@@ -270,7 +270,7 @@ let norm_cstr {coeffs = v ; op = o ; cst = c} idx =
   (match o with
 	| Eq -> Some c , Some c
 	| Ge -> Some c , None) ;
-	    prf = Hyp idx }
+	    prf = Assum idx }
 
 
 (** [load_system l] takes a list of constraints of type [cstr_compat]
@@ -285,7 +285,7 @@ let load_system l =
 
   let vars = List.fold_left (fun vrs (cstr,i) ->
     match norm_cstr cstr i with
-      | Contradiction -> raise (SystemContradiction (Hyp i))
+      | Contradiction -> raise (SystemContradiction (Assum i))
       | Redundant      -> vrs
       | Cstr(vect,info) ->
 	  xadd_cstr  vect info sys ;
@@ -867,7 +867,7 @@ let  mk_proof hyps prf =
 
   let rec mk_proof prf =
     match prf with
-      | Hyp i -> [ ([i, Int 1] , List.nth hyps i) ]
+      | Assum i -> [ ([i, Int 1] , List.nth hyps i) ]
 
       | Elim(v,prf1,prf2) ->
           let prfsl = mk_proof prf1
-- 
cgit v1.2.3


From 95239fa33c5da60080833dabc3ced246680dfdf9 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:56:05 +0200
Subject: Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.or

---
 plugins/micromega/sos.ml     | 19 +++++++++++--------
 plugins/micromega/sos_lib.ml |  2 +-
 2 files changed, 12 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index cc89e2b9d8..7e716258c0 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -282,14 +282,14 @@ let poly_variables (p:poly) =
 (* Order monomials for human presentation.                                   *)
 (* ------------------------------------------------------------------------- *)
 
-let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 or x1 = x2 && k1 > k2;;
+let humanorder_varpow (x1,k1) (x2,k2) = x1 < x2 || x1 = x2 && k1 > k2;;
 
 let humanorder_monomial =
   let rec ord l1 l2 = match (l1,l2) with
     _,[] -> true
   | [],_ -> false
-  | h1::t1,h2::t2 -> humanorder_varpow h1 h2 or h1 = h2 && ord t1 t2 in
-  fun m1 m2 -> m1 = m2 or
+  | h1::t1,h2::t2 -> humanorder_varpow h1 h2 || h1 = h2 && ord t1 t2 in
+  fun m1 m2 -> m1 = m2 ||
                ord (sort humanorder_varpow (graph m1))
                    (sort humanorder_varpow (graph m2));;
 
@@ -466,6 +466,7 @@ let token s =
   >> (fun ((_,t),_) -> t);;
 
 let decimal =
+  let (||) = parser_or in
   let numeral = some isnum in
   let decimalint = atleast 1 numeral >> ((o) Num.num_of_string  implode) in
   let decimalfrac = atleast 1 numeral
@@ -492,6 +493,7 @@ let parse_decimal = mkparser decimal;;
 (* ------------------------------------------------------------------------- *)
 
 let parse_sdpaoutput,parse_csdpoutput =
+  let (||) = parser_or in
   let vector =
     token "{" ++ listof decimal (token ",") "decimal" ++ token "}"
                >> (fun ((_,v),_) -> vector_of_list v) in
@@ -512,6 +514,7 @@ let parse_sdpaoutput,parse_csdpoutput =
 (* ------------------------------------------------------------------------- *)
 
 let sdpa_run_succeeded =
+  let (||) = parser_or in
    let rec skipupto dscr prs inp =
       (dscr ++ prs >> snd
     || some (fun c -> true) ++ skipupto dscr prs >> snd) inp in
@@ -602,7 +605,7 @@ let run_csdp dbg obj mats =
 
 let csdp obj mats =
   let rv,res = run_csdp (!debugging) obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
+  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
    else if rv = 3 then ()
     (* Format.print_string "csdp warning: Reduced accuracy";
      Format.print_newline() *)
@@ -653,7 +656,7 @@ let linear_program_basic a =
   let mats =  List.map (fun j -> diagonal (column j a)) (1--n)
   and obj = vector_const (Int 1) m in
   let rv,res = run_csdp false obj mats in
-  if rv = 1 or rv = 2 then false
+  if rv = 1 || rv = 2 then false
   else if rv = 0 then true
   else failwith "linear_program: An error occurred in the SDP solver";;
 
@@ -667,7 +670,7 @@ let linear_program a b =
   let mats = diagonal b :: List.map (fun j -> diagonal (column j a)) (1--n)
   and obj = vector_const (Int 1) m in
   let rv,res = run_csdp false obj mats in
-  if rv = 1 or rv = 2 then false
+  if rv = 1 || rv = 2 then false
   else if rv = 0 then true
   else failwith "linear_program: An error occurred in the SDP solver";;
 
@@ -968,7 +971,7 @@ let run_csdp dbg nblocks blocksizes obj mats =
 
 let csdp nblocks blocksizes obj mats =
   let rv,res = run_csdp (!debugging) nblocks blocksizes obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
+  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
    else if rv = 3 then ()
     (*Format.print_string "csdp warning: Reduced accuracy";
      Format.print_newline() *)
@@ -1439,7 +1442,7 @@ let run_csdp dbg obj mats =
 
 let csdp obj mats =
   let rv,res = run_csdp (!debugging) obj mats in
-  (if rv = 1 or rv = 2 then failwith "csdp: Problem is infeasible"
+  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
     else if rv = 3 then ()
 (*    (Format.print_string "csdp warning: Reduced accuracy";
      Format.print_newline()) *)
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index f54914f252..9ee3db6e0e 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -525,7 +525,7 @@ let isspace,issep,isbra,issymb,isalpha,isnum,isalnum =
   and isalnum c = Array.get ctable (charcode c) >= 16 in
   isspace,issep,isbra,issymb,isalpha,isnum,isalnum;;
 
-let (||) parser1 parser2 input =
+let parser_or parser1 parser2 input =
   try parser1 input
   with Noparse -> parser2 input;;
 
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 plugins/funind/functional_principles_proofs.ml |  6 ---
 plugins/ltac/extratactics.ml4                  |  2 -
 plugins/ltac/profile_ltac.ml                   |  1 -
 plugins/ltac/tacentries.ml                     |  3 --
 plugins/ltac/tacintern.ml                      |  6 ---
 plugins/ltac/tacinterp.ml                      |  6 ---
 plugins/nsatz/ideal.ml                         | 57 --------------------------
 plugins/nsatz/nsatz.ml                         | 28 -------------
 plugins/setoid_ring/newring.ml                 |  2 -
 plugins/ssrmatching/ssrmatching.ml4            | 21 ----------
 plugins/ssrmatching/ssrmatching.mli            |  1 -
 11 files changed, 133 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8dae17d69e..df81bc78c4 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -19,12 +19,6 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
-let local_assum (na, t) =
-  RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t)
-
-let local_def (na, b, t) =
-  RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
-
 (* let msgnl = Pp.msgnl *)
 
 (*
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..35cfe8b542 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -52,8 +52,6 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
-let clause = Pltac.clause_dft_concl
-
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
 -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index bcb28f77ce..a853576f25 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -136,7 +136,6 @@ let feedback_results results =
 let format_sec x = (Printf.sprintf "%.3fs" x)
 let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
 let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
-let padr n s = str s ++ ws (max 0 (n - utf8_length s))
 let padr_with c n s =
   let ulength = utf8_length s in
   str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 8cda73b4bf..ef1d69d35b 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -88,9 +88,6 @@ let rec parse_user_entry s sep =
   else
     Uentry s
 
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
 let interp_entry_name interp symb =
   let rec eval = function
   | Ulist1 e -> Ulist1 (eval e)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3f83f104e9..75227def0f 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -118,12 +118,6 @@ let intern_constr_reference strict ist = function
       GRef (loc,locate_global_with_alias lqid,None), 
 	if strict then None else Some (CRef (r,None))
 
-let intern_move_location ist = function
-  | MoveAfter id -> MoveAfter (intern_hyp ist id)
-  | MoveBefore id -> MoveBefore (intern_hyp ist id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 (* Internalize an isolated reference in position of tactic *)
 
 let intern_isolated_global_tactic_reference r =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 50f43931e9..fcdf7bb2cd 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -436,12 +436,6 @@ let interp_hyp_list_as_list ist env sigma (loc,id as x) =
 let interp_hyp_list ist env sigma l =
   List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l)
 
-let interp_move_location ist env sigma = function
-  | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id)
-  | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 let interp_reference ist env sigma = function
   | ArgArg (_,r) -> r
   | ArgVar (loc, id) ->
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index b1ff59e780..41f2edfcf1 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -153,7 +153,6 @@ module Make (P:Polynom.S) = struct
   type coef = P.t
   let coef0 = P.of_num (Num.Int 0)
   let coef1 = P.of_num (Num.Int 1)
-  let coefm1 = P.of_num (Num.Int (-1))
   let string_of_coef c = "["^(P.to_string c)^"]"
 
 (***********************************************************************
@@ -252,59 +251,6 @@ let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
   in 
   (stringP p true)
 
-
-
-let print_pol zeroP hdP tlP coefterm monterm string_of_coef
-    dimmon string_of_exp lvar p =
-
-  let rec print_mon m coefone =
-    let s=ref [] in
-    for i=1 to (dimmon m) do
-      (match (string_of_exp m i) with
-        "0" -> ()
-      | "1" -> s:= (!s) @ [(getvar lvar (i-1))]
-      | e -> s:= (!s) @ [((getvar lvar (i-1)) ^ "^" ^ e)]);
-    done;
-    (match !s with
-      [] -> if coefone 
-      then print_string "1"
-      else ()
-    | l -> if coefone 
-    then print_string (String.concat "*" l)
-    else (print_string "*"; 
-          print_string (String.concat "*" l)))
-  and print_term t start = let a = coefterm t and m = monterm t in
-  match (string_of_coef a) with
-    "0" -> ()
-  | "1" ->(match start with
-      true -> print_mon m true
-    |false -> (print_string "+ ";
-               print_mon m true))
-  | "-1" ->(print_string "-";print_space();print_mon m true)
-  | c -> if (String.get c 0)='-'
-  then (print_string "- ";
-        print_string (String.sub c 1 
-                        ((String.length c)-1));
-        print_mon m false)
-  else (match start with
-    true -> (print_string c;print_mon m false)
-  |false -> (print_string "+ ";
-             print_string c;print_mon m false))
-  and printP p start = 
-    if (zeroP p)
-    then (if start 
-    then print_string("0")
-    else ())
-    else (print_term (hdP p) start;
-          if start then open_hovbox 0;
-          print_space();
-          print_cut();
-          printP (tlP p) false)
-  in open_hovbox 3;
-  printP p true;
-  print_flush()
-
-
 let stringP metadata (p : poly) =
   string_of_pol 
     (fun p -> match p with [] -> true | _ -> false)
@@ -595,9 +541,6 @@ let addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat decon
  critical pairs/s-polynomials
  *)
 
-let ordcpair ((i1,j1),m1) ((i2,j2),m2) =
-  compare_mon m1 m2 
-
 module CPair =
 struct
 type t = (int * int) * Monomial.t
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index a5b0166116..632b9dac14 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -22,7 +22,6 @@ open Utile
 let num_0 = Int 0
 and num_1 = Int 1
 and num_2 = Int 2
-and num_10 = Int 10
 
 let numdom r =
   let r' = Ratio.normalize_ratio (ratio_of_num r) in
@@ -35,7 +34,6 @@ module BigInt = struct
   type t = big_int
   let of_int = big_int_of_int
   let coef0 = of_int 0
-  let coef1 = of_int 1
   let of_num = Num.big_int_of_num
   let to_num = Num.num_of_big_int
   let equal = eq_big_int
@@ -49,7 +47,6 @@ module BigInt = struct
   let div = div_big_int
   let modulo = mod_big_int
   let to_string = string_of_big_int
-  let to_int x = int_of_big_int x
   let hash x =
     try (int_of_big_int x)
     with Failure _ -> 1
@@ -61,15 +58,6 @@ module BigInt = struct
     then a
     else if lt a b then pgcd b a else pgcd b (modulo a b)
 
-
-  (* signe du pgcd = signe(a)*signe(b) si non nuls. *)
-  let pgcd2 a b =
-    if equal a coef0 then b
-    else if equal b coef0 then a
-    else let c = pgcd (abs a) (abs b) in
-    if ((lt coef0 a)&&(lt b coef0))
-      ||((lt coef0 b)&&(lt a coef0))
-    then opp c else c
 end
 
 (*
@@ -146,8 +134,6 @@ let mul = function
   | (Const n,q) when eq_num n num_1 -> q
   | (p,q) -> Mul(p,q)
 
-let unconstr = mkRel 1
-
 let tpexpr =
   lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
 let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc")
@@ -271,20 +257,6 @@ let set_nvars_term nvars t =
     | Pow (t1,n) ->  aux t1 nvars
   in aux t nvars
 
-let string_of_term p =
-  let rec aux p =
-    match p with
-    | Zero -> "0"
-    | Const r -> string_of_num r
-    | Var v -> "x"^v
-    | Opp t1 -> "(-"^(aux t1)^")"
-    | Add (t1,t2) -> "("^(aux t1)^"+"^(aux t2)^")"
-    | Sub (t1,t2) ->  "("^(aux t1)^"-"^(aux t2)^")"
-    | Mul (t1,t2) ->  "("^(aux t1)^"*"^(aux t2)^")"
-    | Pow (t1,n) ->  (aux t1)^"^"^(string_of_int n)
-  in aux p
-
-
 (***********************************************************************
    Coefficients: recursive polynomials
  *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index dd68eac24c..6e072e8317 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -279,8 +279,6 @@ let my_constant c =
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
-let new_ring_path =
-  DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let znew_ring_path =
   DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index fc7963b2d3..60c199bf51 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -90,8 +90,6 @@ let pp s = !pp_ref s
 let env_size env = List.length (Environ.named_context env)
 let safeDestApp c =
   match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |]
-let get_index = function ArgArg i -> i | _ ->
-  CErrors.anomaly (str"Uninterpreted index")
 (* Toplevel constr must be globalized twice ! *)
 let glob_constr ist genv = function
   | _, Some ce ->
@@ -304,8 +302,6 @@ let unif_EQ_args env sigma pa a =
 
 let unif_HO env ise p c = Evarconv.the_conv_x env p c ise
 
-let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env p c ise
-
 let unif_HO_args env ise0 pa i ca =
   let n = Array.length pa in
   let rec loop ise j =
@@ -371,11 +367,6 @@ let unif_end env sigma0 ise0 pt ok =
     let s, uc', t = nf_open_term sigma0 ise2 t in
     s, Evd.union_evar_universe_context uc uc', t
 
-let pf_unif_HO gl sigma pt p c =
-  let env = pf_env gl in
-  let ise = unif_HO env (create_evar_defs sigma) p c in
-  unif_end env (project gl) ise pt (fun _ -> true)
-
 let unify_HO env sigma0 t1 t2 =
   let sigma = unif_HO env sigma0 t1 t2 in
   let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in
@@ -440,10 +431,6 @@ let all_ok _ _ = true
 let proj_nparams c =
   try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
 
-let isFixed c = match kind_of_term c with
-  | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true
-  | _ -> false
-
 let isRigid c = match kind_of_term c with
   | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
   | _ -> false
@@ -917,13 +904,6 @@ let pp_pattern (sigma, p) =
 let pr_cpattern = pr_term
 let pr_rpattern _ _ _ = pr_pattern
 
-let pr_option f = function None -> mt() | Some x -> f x
-let pr_ssrpattern _ _ _ = pr_option pr_pattern
-let pr_pattern_squarep = pr_option (fun r -> str "[" ++ pr_pattern r ++ str "]")
-let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep
-let pr_pattern_roundp = pr_option (fun r -> str "(" ++ pr_pattern r ++ str ")")
-let pr_ssrpattern_roundp  _ _ _ = pr_pattern_roundp
-
 let wit_rpatternty = add_genarg "rpatternty" pr_pattern
 
 let glob_ssrterm gs = function
@@ -1045,7 +1025,6 @@ let interp_wit wit ist gl x =
   let arg = interp_genarg ist globarg in
   let (sigma, arg) = of_ftactic arg gl in
   sigma, Value.cast (topwit wit) arg
-let interp_constr = interp_wit wit_constr
 let interp_open_constr ist gl gc =
   interp_wit wit_open_constr ist gl gc
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 894cdb9438..1f984b1609 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -226,7 +226,6 @@ val loc_of_cpattern : cpattern -> Loc.t
 val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern
-val cpattern_of_id : Names.variable -> cpattern
 val pr_constr_pat : constr -> Pp.std_ppcmds
 val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma
 val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma
-- 
cgit v1.2.3


From 528c237b658dbba896a1fe0041990cc7fec9c4c8 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:07:32 +0200
Subject: Add [_] prefix to unused values which maybe should be kept

---
 plugins/ltac/tauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index dc7ee6a234..e86d1c7283 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -242,7 +242,7 @@ let tauto_uniform_unit_flags = {
 }
 
 (* This is the compatibility mode (not used) *)
-let tauto_legacy_flags = {
+let _tauto_legacy_flags = {
   binary_mode = true;
   binary_mode_bugged_detection = true;
   strict_in_contravariant_hyp = true;
-- 
cgit v1.2.3


From 9be835c4f16b3bc08ff9540a6854ced2d8185cb2 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:09:05 +0200
Subject: Remove unused constructors

---
 plugins/ssrmatching/ssrmatching.ml4 | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 60c199bf51..f146fbb118 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -435,8 +435,6 @@ let isRigid c = match kind_of_term c with
   | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
   | _ -> false
 
-exception UndefPat
-
 let hole_var = mkVar (id_of_string "_")
 let pr_constr_pat c0 =
   let rec wipe_evar c =
-- 
cgit v1.2.3


From e1d2a898feacbe4bd363818f259bce5fd74c2ee7 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:09:23 +0200
Subject: Micromega: do not use Filename.temp_dir_path, remove unused values

---
 plugins/micromega/sos.ml     | 257 ++-----------------------------------------
 plugins/micromega/sos_lib.ml |   2 +-
 2 files changed, 11 insertions(+), 248 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 7e716258c0..e1ceabe9e2 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -21,8 +21,6 @@ let debugging = ref false;;
 
 exception Sanity;;
 
-exception Unsolvable;;
-
 (* ------------------------------------------------------------------------- *)
 (* Turn a rational into a decimal string with d sig digits.                  *)
 (* ------------------------------------------------------------------------- *)
@@ -99,28 +97,11 @@ let vector_const c n =
   if c =/ Int 0 then vector_0 n
   else (n,itlist (fun k -> k |-> c) (1--n) undefined :vector);;
 
-let vector_1 = vector_const (Int 1);;
-
 let vector_cmul c (v:vector) =
   let n = dim v in
   if c =/ Int 0 then vector_0 n
   else n,mapf (fun x -> c */ x) (snd v)
 
-let vector_neg (v:vector) = (fst v,mapf minus_num (snd v) :vector);;
-
-let vector_add (v1:vector) (v2:vector) =
-  let m = dim v1 and n = dim v2 in
-  if m <> n then failwith "vector_add: incompatible dimensions" else
-  (n,combine (+/) (fun x -> x =/ Int 0) (snd v1) (snd v2) :vector);;
-
-let vector_sub v1 v2 = vector_add v1 (vector_neg v2);;
-
-let vector_dot (v1:vector) (v2:vector) =
-  let m = dim v1 and n = dim v2 in
-  if m <> n then failwith "vector_add: incompatible dimensions" else
-  foldl (fun a i x -> x +/ a) (Int 0)
-        (combine ( */ ) (fun x -> x =/ Int 0) (snd v1) (snd v2));;
-
 let vector_of_list l =
   let n = List.length l in
   (n,itlist2 (|->) (1--n) l undefined :vector);;
@@ -133,13 +114,6 @@ let matrix_0 (m,n) = ((m,n),undefined:matrix);;
 
 let dimensions (m:matrix) = fst m;;
 
-let matrix_const c (m,n as mn) =
-  if m <> n then failwith "matrix_const: needs to be square"
-  else if c =/ Int 0 then matrix_0 mn
-  else (mn,itlist (fun k -> (k,k) |-> c) (1--n) undefined :matrix);;
-
-let matrix_1 = matrix_const (Int 1);;
-
 let matrix_cmul c (m:matrix) =
   let (i,j) = dimensions m in
   if c =/ Int 0 then matrix_0 (i,j)
@@ -152,8 +126,6 @@ let matrix_add (m1:matrix) (m2:matrix) =
   if d1 <> d2 then failwith "matrix_add: incompatible dimensions"
   else (d1,combine (+/) (fun x -> x =/ Int 0) (snd m1) (snd m2) :matrix);;
 
-let matrix_sub m1 m2 = matrix_add m1 (matrix_neg m2);;
-
 let row k (m:matrix) =
   let i,j = dimensions m in
   (j,
@@ -166,20 +138,10 @@ let column k (m:matrix) =
    foldl (fun a (i,j) c -> if j = k then (i |-> c) a else a) undefined (snd m)
    : vector);;
 
-let transp (m:matrix) =
-  let i,j = dimensions m in
-  ((j,i),foldl (fun a (i,j) c -> ((j,i) |-> c) a) undefined (snd m) :matrix);;
-
 let diagonal (v:vector) =
   let n = dim v in
   ((n,n),foldl (fun a i c -> ((i,i) |-> c) a) undefined (snd v) : matrix);;
 
-let matrix_of_list l =
-  let m = List.length l in
-  if m = 0 then matrix_0 (0,0) else
-  let n = List.length (List.hd l) in
-  (m,n),itern 1 l (fun v i -> itern 1 v (fun c j -> (i,j) |-> c)) undefined;;
-
 (* ------------------------------------------------------------------------- *)
 (* Monomials.                                                                *)
 (* ------------------------------------------------------------------------- *)
@@ -195,24 +157,8 @@ let monomial_var x = (x |=> 1 :monomial);;
 let (monomial_mul:monomial->monomial->monomial) =
   combine (+) (fun x -> false);;
 
-let monomial_pow (m:monomial) k =
-  if k = 0 then monomial_1
-  else mapf (fun x -> k * x) m;;
-
-let monomial_divides (m1:monomial) (m2:monomial) =
-  foldl (fun a x k -> tryapplyd m2 x 0 >= k && a) true m1;;
-
-let monomial_div (m1:monomial) (m2:monomial) =
-  let m = combine (+) (fun x -> x = 0) m1 (mapf (fun x -> -x) m2) in
-  if foldl (fun a x k -> k >= 0 && a) true m then m
-  else failwith "monomial_div: non-divisible";;
-
 let monomial_degree x (m:monomial) = tryapplyd m x 0;;
 
-let monomial_lcm (m1:monomial) (m2:monomial) =
-  (itlist (fun x -> x |-> max (monomial_degree x m1) (monomial_degree x m2))
-          (union (dom m1) (dom m2)) undefined :monomial);;
-
 let monomial_multidegree (m:monomial) = foldl (fun a x k -> k + a) 0 m;;
 
 let monomial_variables m = dom m;;
@@ -252,12 +198,6 @@ let poly_cmmul (c,m) (p:poly) =
 let poly_mul (p1:poly) (p2:poly) =
   foldl (fun a m c -> poly_add (poly_cmmul (c,m) p2) a) poly_0 p1;;
 
-let poly_div (p1:poly) (p2:poly) =
-  if not(poly_isconst p2) then failwith "poly_div: non-constant" else
-  let c = eval undefined p2 in
-  if c =/ Int 0 then failwith "poly_div: division by zero"
-  else poly_cmul (Int 1 // c) p1;;
-
 let poly_square p = poly_mul p p;;
 
 let rec poly_pow p k =
@@ -266,10 +206,6 @@ let rec poly_pow p k =
   else let q = poly_square(poly_pow p (k / 2)) in
        if k mod 2 = 1 then poly_mul p q else q;;
 
-let poly_exp p1 p2 =
-  if not(poly_isconst p2) then failwith "poly_exp: not a constant" else
-  poly_pow p1 (Num.int_of_num (eval undefined p2));;
-
 let degree x (p:poly) = foldl (fun a m c -> max (monomial_degree x m) a) 0 p;;
 
 let multidegree (p:poly) =
@@ -297,42 +233,8 @@ let humanorder_monomial =
 (* Conversions to strings.                                                   *)
 (* ------------------------------------------------------------------------- *)
 
-let string_of_vector min_size max_size (v:vector) =
-  let n_raw = dim v in
-  if n_raw = 0 then "[]" else
-  let n = max min_size (min n_raw max_size) in
-  let xs = List.map ((o) string_of_num (element v)) (1--n) in
-  "[" ^ end_itlist (fun s t -> s ^ ", " ^ t) xs ^
-  (if n_raw > max_size then ", ...]" else "]");;
-
-let string_of_matrix max_size (m:matrix) =
-  let i_raw,j_raw = dimensions m in
-  let i = min max_size i_raw and j = min max_size j_raw in
-  let rstr = List.map (fun k -> string_of_vector j j (row k m)) (1--i) in
-  "["^end_itlist(fun s t -> s^";\n "^t) rstr ^
-  (if j > max_size then "\n ...]" else "]");;
-
 let string_of_vname (v:vname): string = (v: string);;
 
-let rec string_of_term t =
-  match t with
-  Opp t1 -> "(- " ^ string_of_term t1 ^ ")"
-| Add (t1, t2) ->
-   "(" ^ (string_of_term t1) ^ " + " ^ (string_of_term t2) ^ ")"
-| Sub (t1, t2) ->
-   "(" ^ (string_of_term t1) ^ " - " ^ (string_of_term t2) ^ ")"
-| Mul (t1, t2) ->
-   "(" ^ (string_of_term t1) ^ " * " ^ (string_of_term t2) ^ ")"
-| Inv t1 -> "(/ " ^ string_of_term t1 ^ ")"
-| Div (t1, t2) ->
-   "(" ^ (string_of_term t1) ^ " / " ^ (string_of_term t2) ^ ")"
-| Pow (t1, n1) ->
-   "(" ^ (string_of_term t1) ^ " ^ " ^ (string_of_int n1) ^ ")"
-| Zero -> "0"
-| Var v -> "x" ^ (string_of_vname v)
-| Const x -> string_of_num x;;
-
-
 let string_of_varpow x k =
   if k = 1 then string_of_vname x else string_of_vname x^"^"^string_of_int k;;
 
@@ -363,6 +265,7 @@ let string_of_poly (p:poly) =
 (* Printers.                                                                 *)
 (* ------------------------------------------------------------------------- *)
 
+(*
 let print_vector v = Format.print_string(string_of_vector 0 20 v);;
 
 let print_matrix m = Format.print_string(string_of_matrix 20 m);;
@@ -371,7 +274,6 @@ let print_monomial m = Format.print_string(string_of_monomial m);;
 
 let print_poly m = Format.print_string(string_of_poly m);;
 
-(*
 #install_printer print_vector;;
 #install_printer print_matrix;;
 #install_printer print_monomial;;
@@ -410,19 +312,6 @@ let sdpa_of_vector (v:vector) =
   let strs = List.map (o (decimalize 20)  (element v)) (1--n) in
   end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";;
 
-(* ------------------------------------------------------------------------- *)
-(* String for block diagonal matrix numbered k.                              *)
-(* ------------------------------------------------------------------------- *)
-
-let sdpa_of_blockdiagonal k m =
-  let pfx = string_of_int k ^" " in
-  let ents =
-    foldl (fun a (b,i,j) c -> if i > j then a else ((b,i,j),c)::a) [] m in
-  let entss = sort (increasing fst) ents in
-  itlist (fun ((b,i,j),c) a ->
-     pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
-     " " ^ decimalize 20 c ^ "\n" ^ a) entss "";;
-
 (* ------------------------------------------------------------------------- *)
 (* String for a matrix numbered k, in SDPA sparse format.                    *)
 (* ------------------------------------------------------------------------- *)
@@ -486,13 +375,11 @@ let mkparser p s =
   let x,rst = p(explode s) in
   if rst = [] then x else failwith "mkparser: unparsed input";;
 
-let parse_decimal = mkparser decimal;;
-
 (* ------------------------------------------------------------------------- *)
 (* Parse back a vector.                                                      *)
 (* ------------------------------------------------------------------------- *)
 
-let parse_sdpaoutput,parse_csdpoutput =
+let _parse_sdpaoutput, parse_csdpoutput =
   let (||) = parser_or in
   let vector =
     token "{" ++ listof decimal (token ",") "decimal" ++ token "}"
@@ -509,25 +396,11 @@ let parse_sdpaoutput,parse_csdpoutput =
     (a " " ++ a "\n" ++ ignore) >> ((o) vector_of_list fst) in
   mkparser sdpaoutput,mkparser csdpoutput;;
 
-(* ------------------------------------------------------------------------- *)
-(* Also parse the SDPA output to test success (CSDP yields a return code).   *)
-(* ------------------------------------------------------------------------- *)
-
-let sdpa_run_succeeded =
-  let (||) = parser_or in
-   let rec skipupto dscr prs inp =
-      (dscr ++ prs >> snd
-    || some (fun c -> true) ++ skipupto dscr prs >> snd) inp in
-  let prs = skipupto (word "phase.value" ++ token "=")
-                     (possibly (a "p") ++ possibly (a "d") ++
-                      (word "OPT" || word "FEAS")) in
-  fun s -> try ignore (prs (explode s)); true with Noparse -> false;;
-
 (* ------------------------------------------------------------------------- *)
 (* The default parameters. Unfortunately this goes to a fixed file.          *)
 (* ------------------------------------------------------------------------- *)
 
-let sdpa_default_parameters =
+let _sdpa_default_parameters =
 "100     unsigned int maxIteration;\
 \n1.0E-7  double 0.0 < epsilonStar;\
 \n1.0E2   double 0.0 < lambdaStar;\
@@ -558,7 +431,7 @@ let sdpa_alt_parameters =
 \n1.0E-7  double 0.0 < epsilonDash;\
 \n";;
 
-let sdpa_params = sdpa_alt_parameters;;
+let _sdpa_params = sdpa_alt_parameters;;
 
 (* ------------------------------------------------------------------------- *)
 (* CSDP parameters; so far I'm sticking with the defaults.                   *)
@@ -591,10 +464,10 @@ let run_csdp dbg obj mats =
   let input_file = Filename.temp_file "sos" ".dat-s" in
   let output_file =
     String.sub input_file 0 (String.length input_file - 6) ^ ".out"
-  and params_file = Filename.concat (!temp_path) "param.csdp" in
+  and params_file = Filename.concat temp_path "param.csdp" in
   file_of_string input_file (sdpa_of_problem "" obj mats);
   file_of_string params_file csdp_params;
-  let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^
+  let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^
                         " " ^ output_file ^
                        (if dbg then "" else "> /dev/null")) in
   let op = string_of_file output_file in
@@ -603,16 +476,6 @@ let run_csdp dbg obj mats =
     else (Sys.remove input_file; Sys.remove output_file));
     rv,res);;
 
-let csdp obj mats =
-  let rv,res = run_csdp (!debugging) obj mats in
-  (if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible"
-   else if rv = 3 then ()
-    (* Format.print_string "csdp warning: Reduced accuracy";
-     Format.print_newline() *)
-   else if rv <> 0 then failwith("csdp: error "^string_of_int rv)
-   else ());
-  res;;
-
 (* ------------------------------------------------------------------------- *)
 (* Try some apparently sensible scaling first. Note that this is purely to   *)
 (* get a cleaner translation to floating-point, and doesn't affect any of    *)
@@ -660,20 +523,6 @@ let linear_program_basic a =
   else if rv = 0 then true
   else failwith "linear_program: An error occurred in the SDP solver";;
 
-(* ------------------------------------------------------------------------- *)
-(* Alternative interface testing A x >= b for matrix A, vector b.            *)
-(* ------------------------------------------------------------------------- *)
-
-let linear_program a b =
-  let m,n = dimensions a in
-  if dim b <> m then failwith "linear_program: incompatible dimensions" else
-  let mats = diagonal b :: List.map (fun j -> diagonal (column j a)) (1--n)
-  and obj = vector_const (Int 1) m in
-  let rv,res = run_csdp false obj mats in
-  if rv = 1 || rv = 2 then false
-  else if rv = 0 then true
-  else failwith "linear_program: An error occurred in the SDP solver";;
-
 (* ------------------------------------------------------------------------- *)
 (* Test whether a point is in the convex hull of others. Rather than use     *)
 (* computational geometry, express as linear inequalities and call CSDP.     *)
@@ -718,40 +567,6 @@ let equation_eval assig eq =
   let value v = apply assig v in
   foldl (fun a v c -> a +/ value(v) */ c) (Int 0) eq;;
 
-(* ------------------------------------------------------------------------- *)
-(* Eliminate among linear equations: return unconstrained variables and      *)
-(* assignments for the others in terms of them. We give one pseudo-variable  *)
-(* "one" that's used for a constant term.                                    *)
-(* ------------------------------------------------------------------------- *)
-
-let failstore = ref [];;
-
-let eliminate_equations =
-  let rec extract_first p l =
-    match l with
-      [] -> failwith "extract_first"
-    | h::t -> if p(h) then h,t else
-              let k,s = extract_first p t in
-              k,h::s in
-  let rec eliminate vars dun eqs =
-    match vars with
-      [] -> if forall is_undefined eqs then dun
-            else (failstore := [vars,dun,eqs]; raise Unsolvable)
-    | v::vs ->
-            try let eq,oeqs = extract_first (fun e -> defined e v) eqs in
-                let a = apply eq v in
-                let eq' = equation_cmul (Int(-1) // a) (undefine v eq) in
-                let elim e =
-                  let b = tryapplyd e v (Int 0) in
-                  if b =/ Int 0 then e else
-                  equation_add e (equation_cmul (minus_num b // a) eq) in
-                eliminate vs ((v |-> eq') (mapf elim dun)) (List.map elim oeqs)
-            with Failure _ -> eliminate vs dun eqs in
-  fun one vars eqs ->
-    let assig = eliminate vars undefined eqs in
-    let vs = foldl (fun a x f -> subtract (dom f) [one] @ a) [] assig in
-    setify vs,assig;;
-
 (* ------------------------------------------------------------------------- *)
 (* Eliminate all variables, in an essentially arbitrary order.               *)
 (* ------------------------------------------------------------------------- *)
@@ -782,18 +597,6 @@ let eliminate_all_equations one =
     let vs = foldl (fun a x f -> subtract (dom f) [one] @ a) [] assig in
     setify vs,assig;;
 
-(* ------------------------------------------------------------------------- *)
-(* Solve equations by assigning arbitrary numbers.                           *)
-(* ------------------------------------------------------------------------- *)
-
-let solve_equations one eqs =
-  let vars,assigs = eliminate_all_equations one eqs in
-  let vfn = itlist (fun v -> (v |-> Int 0)) vars (one |=> Int(-1)) in
-  let ass =
-    combine (+/) (fun c -> false) (mapf (equation_eval vfn) assigs) vfn in
-  if forall (fun e -> equation_eval ass e =/ Int 0) eqs
-  then undefine one ass else raise Sanity;;
-
 (* ------------------------------------------------------------------------- *)
 (* Hence produce the "relevant" monomials: those whose squares lie in the    *)
 (* Newton polytope of the monomials in the input. (This is enough according  *)
@@ -900,19 +703,6 @@ let epoly_pmul p q acc =
                         (m |-> equation_add (equation_cmul c e) es) b)
                  a q) acc p;;
 
-(* ------------------------------------------------------------------------- *)
-(* Usual operations on equation-parametrized poly.                           *)
-(* ------------------------------------------------------------------------- *)
-
-let epoly_cmul c l =
-  if c =/ Int 0 then undefined else mapf (equation_cmul c) l;;
-
-let epoly_neg = epoly_cmul (Int(-1));;
-
-let epoly_add = combine equation_add is_undefined;;
-
-let epoly_sub p q = epoly_add p (epoly_neg q);;
-
 (* ------------------------------------------------------------------------- *)
 (* Convert regular polynomial. Note that we treat (0,0,0) as -1.             *)
 (* ------------------------------------------------------------------------- *)
@@ -956,11 +746,11 @@ let run_csdp dbg nblocks blocksizes obj mats =
   let input_file = Filename.temp_file "sos" ".dat-s" in
   let output_file =
     String.sub input_file 0 (String.length input_file - 6) ^ ".out"
-  and params_file = Filename.concat (!temp_path) "param.csdp" in
+  and params_file = Filename.concat temp_path "param.csdp" in
   file_of_string input_file
    (sdpa_of_blockproblem "" nblocks blocksizes obj mats);
   file_of_string params_file csdp_params;
-  let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^
+  let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^
                         " " ^ output_file ^
                        (if dbg then "" else "> /dev/null")) in
   let op = string_of_file output_file in
@@ -991,8 +781,6 @@ let bmatrix_cmul c bm =
 
 let bmatrix_neg = bmatrix_cmul (Int(-1));;
 
-let bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);;
-
 (* ------------------------------------------------------------------------- *)
 (* Smash a block matrix into components.                                     *)
 (* ------------------------------------------------------------------------- *)
@@ -1104,15 +892,6 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
   if not(is_undefined sanity) then raise Sanity else
   cfs,List.map (fun (a,b) -> snd a,b) msq;;
 
-(* ------------------------------------------------------------------------- *)
-(* Iterative deepening.                                                      *)
-(* ------------------------------------------------------------------------- *)
-
-let rec deepen f n =
-  try print_string "Searching with depth limit ";
-      print_int n; print_newline(); f n
-  with Failure _ -> deepen f (n + 1);;
-
 (* ------------------------------------------------------------------------- *)
 (* The ordering so we can create canonical HOL polynomials.                  *)
 (* ------------------------------------------------------------------------- *)
@@ -1139,10 +918,6 @@ let monomial_order =
     if deg1 < deg2 then false else if deg1 > deg2 then true
     else lexorder mon1 mon2;;
 
-let dest_poly p =
-  List.map (fun (m,c) -> c,dest_monomial m)
-      (sort (fun (m1,_) (m2,_) -> monomial_order m1 m2) (graph p));;
-
 (* ------------------------------------------------------------------------- *)
 (* Map back polynomials and their composites to HOL.                         *)
 (* ------------------------------------------------------------------------- *)
@@ -1376,9 +1151,6 @@ let rec allpermutations l =
   itlist (fun h acc -> List.map (fun t -> h::t)
                 (allpermutations (subtract l [h])) @ acc) l [];;
 
-let allvarorders l =
-  List.map (fun vlis x -> index x vlis) (allpermutations l);;
-
 let changevariables_monomial zoln (m:monomial) =
   foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;;
 
@@ -1395,15 +1167,6 @@ let sdpa_of_vector (v:vector) =
   let strs = List.map (o (decimalize 20) (element v)) (1--n) in
   end_itlist (fun x y -> x ^ " " ^ y) strs ^ "\n";;
 
-let sdpa_of_blockdiagonal k m =
-  let pfx = string_of_int k ^" " in
-  let ents =
-    foldl (fun a (b,i,j) c -> if i > j then a else ((b,i,j),c)::a) [] m in
-  let entss = sort (increasing fst) ents in
-  itlist (fun ((b,i,j),c) a ->
-     pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
-     " " ^ decimalize 20 c ^ "\n" ^ a) entss "";;
-
 let sdpa_of_matrix k (m:matrix) =
   let pfx = string_of_int k ^ " 1 " in
   let ms = foldr (fun (i,j) c a -> if i > j then a else ((i,j),c)::a)
@@ -1428,10 +1191,10 @@ let run_csdp dbg obj mats =
   let input_file = Filename.temp_file "sos" ".dat-s" in
   let output_file =
     String.sub input_file 0 (String.length input_file - 6) ^ ".out"
-  and params_file = Filename.concat (!temp_path) "param.csdp" in
+  and params_file = Filename.concat temp_path "param.csdp" in
   file_of_string input_file (sdpa_of_problem "" obj mats);
   file_of_string params_file csdp_params;
-  let rv = Sys.command("cd "^(!temp_path)^"; csdp "^input_file ^
+  let rv = Sys.command("cd "^temp_path^"; csdp "^input_file ^
                        " " ^ output_file ^
                        (if dbg then "" else "> /dev/null")) in
   let op = string_of_file output_file in
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index 9ee3db6e0e..6b8b820ac6 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -571,7 +571,7 @@ let finished input =
 
 (* ------------------------------------------------------------------------- *)
 
-let temp_path = ref Filename.temp_dir_name;;
+let temp_path = Filename.get_temp_dir_name ();;
 
 (* ------------------------------------------------------------------------- *)
 (* Convenient conversion between files and (lists of) strings.               *)
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 plugins/firstorder/instances.ml                 |  1 -
 plugins/funind/functional_principles_proofs.mli |  1 -
 plugins/funind/g_indfun.ml4                     |  1 -
 plugins/funind/indfun_common.ml                 |  1 -
 plugins/funind/invfun.ml                        |  1 -
 plugins/funind/merge.ml                         |  1 -
 plugins/ltac/evar_tactics.ml                    |  1 -
 plugins/ltac/extratactics.ml4                   |  1 -
 plugins/ltac/g_auto.ml4                         |  1 -
 plugins/ltac/g_class.ml4                        |  3 ---
 plugins/ltac/pltac.ml                           |  1 -
 plugins/ltac/rewrite.mli                        |  1 -
 plugins/ltac/taccoerce.mli                      |  1 -
 plugins/ltac/tacentries.ml                      |  1 -
 plugins/ltac/tacenv.mli                         |  1 -
 plugins/ltac/tacinterp.ml                       |  1 -
 plugins/ltac/tacinterp.mli                      |  1 -
 plugins/ltac/tactic_debug.mli                   |  1 -
 plugins/micromega/coq_micromega.ml              |  1 -
 plugins/nsatz/ideal.ml                          |  2 --
 plugins/setoid_ring/newring.ml                  |  1 -
 plugins/setoid_ring/newring.mli                 |  3 ---
 plugins/ssrmatching/ssrmatching.ml4             | 14 --------------
 plugins/ssrmatching/ssrmatching.mli             |  1 -
 24 files changed, 42 deletions(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 62f811546d..2b624b9833 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -17,7 +17,6 @@ open Tacmach.New
 open Tactics
 open Tacticals.New
 open Proofview.Notations
-open Termops
 open Reductionops
 open Formula
 open Sequent
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 7ddc84d015..61752aa339 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,5 +1,4 @@
 open Names
-open Term
 
 val prove_princ_for_struct :
   Evd.evar_map ref ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0dccd25d75..b5eacee818 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -8,7 +8,6 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 open Ltac_plugin
 open Util
-open Term
 open Pp
 open Constrexpr
 open Indfun_common
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7b0d7d27d7..c6f5c27458 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -508,7 +508,6 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
 
 let decompose_lam_n sigma n =
-  let open EConstr in
   if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive";
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94ec0a898a..29472cdef3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Ltac_plugin
-open Tacexpr
 open Declarations
 open CErrors
 open Util
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f1ca575856..0af0898a0a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -19,7 +19,6 @@ open Pp
 open Names
 open Term
 open Vars
-open Termops
 open Declarations
 open Glob_term
 open Glob_termops
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 5d3f6df03d..bc9c300e23 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -9,7 +9,6 @@
 open Util
 open Names
 open Term
-open EConstr
 open CErrors
 open Evar_refiner
 open Tacmach
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 35cfe8b542..21419d1f92 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -21,7 +21,6 @@ open Tacexpr
 open Glob_ops
 open CErrors
 open Util
-open Evd
 open Termops
 open Equality
 open Misctypes
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfa8331ff2..50e8255a67 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -16,7 +16,6 @@ open Pcoq.Constr
 open Pltac
 open Hints
 open Tacexpr
-open Proofview.Notations
 open Names
 
 DECLARE PLUGIN "g_auto"
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index ff5e7d5ff2..23ce368eea 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -8,9 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Misctypes
 open Class_tactics
-open Pltac
 open Stdarg
 open Tacarg
 open Names
@@ -95,7 +93,6 @@ END
 (** TODO: DEPRECATE *)
 (* A progress test that allows to see if the evars have changed *)
 open Term
-open Proofview.Goal
 open Proofview.Notations
 
 let rec eq_constr_mod_evars sigma x y =
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1d21118ae8..7e979d269d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Pcoq
 
 (* Main entry for extensions *)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 7a20838a27..6683d753bc 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -14,7 +14,6 @@ open Constrexpr
 open Tacexpr
 open Misctypes
 open Evd
-open Proof_type
 open Tacinterp
 
 (** TODO: document and clean me! *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 9c4ac52657..4a44f86d92 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open EConstr
 open Misctypes
 open Pattern
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index ef1d69d35b..32750383b8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -15,7 +15,6 @@ open Genarg
 open Extend
 open Pcoq
 open Egramml
-open Egramcoq
 open Vernacexpr
 open Libnames
 open Nameops
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 94e14223aa..d1e2a7bbe6 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Genarg
 open Names
 open Tacexpr
 open Geninterp
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fcdf7bb2cd..b8c021f188 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -25,7 +25,6 @@ open Refiner
 open Tacmach.New
 open Tactic_debug
 open Constrexpr
-open Term
 open Termops
 open Tacexpr
 open Genarg
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 1e5f6bd42b..494f36a95a 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Tactic_debug
-open Term
 open EConstr
 open Tacexpr
 open Genarg
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 7745d9b7b6..0b4d35a22a 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -10,7 +10,6 @@ open Environ
 open Pattern
 open Names
 open Tacexpr
-open Term
 open EConstr
 open Evd
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index eb26c5431d..a36607ec38 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -331,7 +331,6 @@ module M =
 struct
 
   open Coqlib
-  open Term
   open Constr
   open EConstr
 
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 41f2edfcf1..a120d4efb2 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -196,8 +196,6 @@ module Hashpol = Hashtbl.Make(
 
 (* A pretty printer for polynomials, with Maple-like syntax. *)
 
-open Format
-
 let getvar lv i =
   try (List.nth lv i)
   with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 6e072e8317..d59ffee546 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -19,7 +19,6 @@ open Environ
 open Libnames
 open Globnames
 open Glob_term
-open Tacticals
 open Tacexpr
 open Coqlib
 open Mod_subst
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 4367d021c0..d9d32c681d 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -7,13 +7,10 @@
 (************************************************************************)
 
 open Names
-open Constr
 open EConstr
 open Libnames
 open Globnames
 open Constrexpr
-open Tacexpr
-open Proof_type
 open Newring_ast
 
 val protect_tac_in : string -> Id.t -> unit Proofview.tactic
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index f146fbb118..72c70750c9 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -21,30 +21,21 @@ open Pp
 open Pcoq
 open Genarg
 open Stdarg
-open Tacarg
 open Term
 open Vars
-open Topconstr
 open Libnames
 open Tactics
 open Tacticals
 open Termops
-open Namegen
 open Recordops
 open Tacmach
-open Coqlib
 open Glob_term
 open Util
 open Evd
-open Extend
-open Goptions
 open Tacexpr
-open Proofview.Notations
 open Tacinterp
 open Pretyping
 open Constr
-open Pltac
-open Extraargs
 open Ppconstr
 open Printer
 
@@ -54,14 +45,9 @@ open Decl_kinds
 open Evar_kinds
 open Constrexpr
 open Constrexpr_ops
-open Notation_term
-open Notation_ops
-open Locus
-open Locusops
 
 DECLARE PLUGIN "ssrmatching_plugin"
 
-type loc = Loc.t
 let dummy_loc = Loc.ghost
 let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
 let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 1f984b1609..638b4e254e 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -4,7 +4,6 @@
 open Genarg
 open Tacexpr
 open Environ
-open Tacmach
 open Evd
 open Proof_type
 open Term
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 plugins/firstorder/g_ground.ml4                |  1 -
 plugins/funind/functional_principles_proofs.ml |  5 +++--
 plugins/funind/indfun_common.ml                |  9 +++------
 plugins/funind/invfun.ml                       | 10 +++++-----
 plugins/funind/recdef.ml                       |  5 +++--
 plugins/ltac/rewrite.ml                        |  2 +-
 plugins/ltac/tauto.ml                          |  1 -
 plugins/omega/omega.ml                         | 10 ++++++----
 8 files changed, 21 insertions(+), 22 deletions(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 8ef6a09d0e..b250175354 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -123,7 +123,6 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives)
 	   (Tacexpr.InHypType id)) *)
 
-open Pp
 open Genarg
 open Ppconstr
 open Printer
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index df81bc78c4..55d361e3d2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -229,12 +229,13 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
   Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
 
 
+exception NoChange
 
 let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
   let nochange ?t' msg  =
     begin
       observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t );
-      failwith "NoChange";
+      raise NoChange;
     end
   in
   let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in
@@ -536,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	      tclTHEN
 		tac
 		(scan_type new_context new_t')
-	    with Failure "NoChange" ->
+	    with NoChange ->
 	      (* Last thing todo : push the rel in the context and continue *)
 	      scan_type (LocalAssum (x,t_x) :: context) t'
 	  end
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c6f5c27458..848b44a603 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -21,12 +21,9 @@ let get_name avoid ?(default="H") = function
   | Name n -> Name n
 
 let array_get_start a =
-  try
-    Array.init
-      (Array.length a - 1)
-      (fun i -> a.(i))
-  with Invalid_argument "index out of bounds" ->
-    invalid_arg "array_get_start"
+  Array.init
+    (Array.length a - 1)
+    (fun i -> a.(i))
 
 let id_of_name = function
     Name id -> id
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 29472cdef3..6c0c28905e 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1025,7 +1025,7 @@ let invfun qhyp f  =
     | Not_found ->  error "No graph found"
     | Option.IsNone  -> error "Cannot use equivalence with graph!"
 
-
+exception NoFunction
 let invfun qhyp f g =
   match f with
     | Some f -> invfun qhyp f g
@@ -1040,23 +1040,23 @@ let invfun qhyp f g =
 		   begin
 		     let f1,_ = decompose_app sigma args.(1) in
 		     try
-		       if not (isConst sigma f1) then failwith "";
+		       if not (isConst sigma f1) then raise NoFunction;
 		       let finfos = find_Function_infos (fst (destConst sigma f1)) in
 		       let f_correct = mkConst(Option.get finfos.correctness_lemma)
 		       and kn = fst finfos.graph_ind
 		       in
 		       functional_inversion kn hid f1 f_correct g
-		     with | Failure "" | Option.IsNone | Not_found ->
+		     with | NoFunction | Option.IsNone | Not_found ->
 		       try
 			 let f2,_ = decompose_app sigma args.(2) in
-			 if not (isConst sigma f2) then failwith "";
+			 if not (isConst sigma f2) then raise NoFunction;
 			 let finfos = find_Function_infos (fst (destConst sigma f2)) in
 			 let f_correct = mkConst(Option.get finfos.correctness_lemma)
 			 and kn = fst finfos.graph_ind
 			 in
 			 functional_inversion kn hid  f2 f_correct g
 		       with
-			 | Failure "" ->
+			 | NoFunction ->
 			     user_err  (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
 			 | Option.IsNone  ->
 			     if do_observe ()
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1e405d2c90..bd30f11596 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1225,6 +1225,7 @@ let get_current_subgoals_types () =
   let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
     sigma, List.map (Goal.V82.abstract_type sigma) sgs
 
+exception EmptySubgoals
 let build_and_l sigma l =
   let and_constr =  Coqlib.build_coq_and () in
   let conj_constr = coq_conj () in
@@ -1246,7 +1247,7 @@ let build_and_l sigma l =
   in
   let l = List.sort compare l in 
   let rec f  = function
-    | [] -> failwith "empty list of subgoals!"
+    | [] -> raise EmptySubgoals
     | [p] -> p,tclIDTAC,1
     | p1::pl ->
 	let c,tac,nb = f pl in
@@ -1432,7 +1433,7 @@ let com_terminate
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type);
-  with Failure "empty list of subgoals!" ->
+  with EmptySubgoals ->
     (* a non recursive function declared with measure ! *)
     tcc_lemma_ref := Not_needed;
     defined ()
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 12a1566e20..9a1615d3f2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -39,7 +39,7 @@ open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 
 (** Typeclass-based generalized rewriting. *)
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index e86d1c7283..4de2081cf8 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -10,7 +10,6 @@ open Term
 open EConstr
 open Hipattern
 open Names
-open Pp
 open Geninterp
 open Misctypes
 open Tacexpr
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index bd991a955c..334b03de1d 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -330,11 +330,13 @@ let omega_mod a b = a - b * floor_div (two * a + b) (two * b)
 let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
   let e = original.body in
   let sigma = new_var_id () in
+  if e == [] then begin
+    display_system print_var [original] ; failwith "TL"
+    end;
   let smallest,var =
-    try
-      List.fold_left (fun (v,p) c ->  if v >? (abs c.c) then abs c.c,c.v else (v,p))
-              (abs (List.hd e).c, (List.hd e).v) (List.tl e)
-    with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
+    List.fold_left (fun (v,p) c ->  if v >? (abs c.c) then abs c.c,c.v else (v,p))
+      (abs (List.hd e).c, (List.hd e).v) (List.tl e)
+  in
   let m = smallest + one in
   let new_eq =
     { constant = omega_mod original.constant m;
-- 
cgit v1.2.3


From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 27 Apr 2017 21:58:52 +0200
Subject: Post-rebase warnings (unused opens and 2 unused values)

---
 plugins/cc/cctac.ml             | 2 --
 plugins/cc/cctac.mli            | 1 -
 plugins/firstorder/formula.ml   | 1 -
 plugins/firstorder/instances.ml | 1 -
 plugins/firstorder/rules.ml     | 1 -
 plugins/firstorder/rules.mli    | 1 -
 plugins/firstorder/sequent.ml   | 1 -
 plugins/firstorder/sequent.mli  | 2 --
 plugins/ltac/g_rewrite.ml4      | 1 -
 plugins/ltac/rewrite.ml         | 1 -
 10 files changed, 12 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 00b31cccee..7c5efaea3a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -15,13 +15,11 @@ open Declarations
 open Term
 open EConstr
 open Vars
-open Tacmach
 open Tactics
 open Typing
 open Ccalgo
 open Ccproof
 open Pp
-open CErrors
 open Util
 open Proofview.Notations
 
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 5099d847b0..b4bb62be8e 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -8,7 +8,6 @@
 (************************************************************************)
 
 open EConstr
-open Proof_type
 
 val proof_tac: Ccproof.proof -> unit Proofview.tactic
 
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index ade94e98e3..9900792cac 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -12,7 +12,6 @@ open Term
 open EConstr
 open Vars
 open Termops
-open Tacmach
 open Util
 open Declarations
 open Globnames
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 2b624b9833..5a1e7c26a1 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -10,7 +10,6 @@ open Unify
 open Rules
 open CErrors
 open Util
-open Term
 open EConstr
 open Vars
 open Tacmach.New
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e0d2c38a73..86a6770070 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open EConstr
 open Vars
 open Tacmach.New
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 80a7ae2c25..fb21730830 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -8,7 +8,6 @@
 
 open Term
 open EConstr
-open Tacmach
 open Names
 open Globnames
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 59b842c825..2d18b66054 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -12,7 +12,6 @@ open CErrors
 open Util
 open Formula
 open Unify
-open Tacmach
 open Globnames
 open Pp
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 18d68f54f9..6ed251f34e 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -6,10 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Formula
-open Tacmach
 open Globnames
 
 module OrderedConstr: Set.OrderedType with type t=Constr.t
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fdcaedab3a..ac979bcf89 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -18,7 +18,6 @@ open Glob_term
 open Geninterp
 open Extraargs
 open Tacmach
-open Tacticals
 open Proofview.Notations
 open Rewrite
 open Stdarg
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9a1615d3f2..5630a2d7b6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -17,7 +17,6 @@ open EConstr
 open Vars
 open Reduction
 open Tacticals.New
-open Tacmach
 open Tactics
 open Pretype_errors
 open Typeclasses
-- 
cgit v1.2.3


From b12af1535c0ba8cab23e7f9ff18f75688c0e523c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Wed, 3 May 2017 19:16:48 +0200
Subject: Make congruence reuse discriminate instead of rolling its own.

This changes the produced terms a bit, eg

Axiom T : Type.
Lemma foo : true = false -> T.
Proof. congruence. Qed.

used to produce

fun H : true = false =>
let Heq := H : true = false in
@eq_rect Type True (fun X : Type => X) I T
  (@f_equal bool Type (fun t : bool => if t then True else T) true false Heq)

now produces

fun H : true = false =>
let Heq : true = false := H in
let H0 : False := @eq_ind bool true (fun e : bool => if e then True else False) I false Heq in
False_rect T H0

i.e. instead of proving [True = T] by [f_equal] then transporting [I]
across this identity, it now proves [False] by [eq_ind] then uses exfalso.
---
 plugins/cc/cctac.ml | 27 ++++++---------------------
 1 file changed, 6 insertions(+), 21 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7c5efaea3a..1cb417bf47 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -397,33 +397,18 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
        simplest_elim false_t]
   end }
 
-let discriminate_tac (cstr,u as cstru) p =
+(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *)
+let discriminate_tac cstru p =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+    let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
     let env = Proofview.Goal.env gl in
-    let concl = Proofview.Goal.concl gl in
-    let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
-    let identity = Universes.constr_of_global (Lazy.force _I) in
-    let identity = EConstr.of_constr identity in
-    let trivial = Universes.constr_of_global (Lazy.force _True) in
-    let trivial = EConstr.of_constr trivial in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
-    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
-    let outtype = mkSort outtype in
-    let pred = mkLambda(Name xid,outtype,mkRel 1) in
+    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in
     let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
-    let proj = build_projection intype cstru trivial concl gl in
-    let injt = app_global _f_equal
-			[|intype;outtype;proj;t1;t2;mkVar hid|] in
-    let endt k =
-      injt (fun injt ->
-            app_global _eq_rect
-		       [|outtype;trivial;pred;identity;concl;injt|] k) in
-    let neweq = app_global _eq [|intype;t1;t2|] in
+    let neweq=app_global _eq [|intype;lhs;rhs|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
 			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
-      [proof_tac p; endt refine_exact_check])
+      [proof_tac p; Equality.discrHyp hid])
   end }
 
 (* wrap everything *)
-- 
cgit v1.2.3


From 8f4d79115c3686de41e20c41ef6dbce8b8546366 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Feb 2017 18:51:36 +0100
Subject: Adding an option "Set Ltac Batch Debug" to additionally run Ltac
 debug in batch mode.

---
 plugins/ltac/tactic_debug.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index dffeade298..dac15ff79e 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -85,6 +85,19 @@ let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
 let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
 let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
 
+let batch = ref false
+
+open Goptions
+
+let _ =
+  declare_bool_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "Ltac batch debug";
+      optkey   = ["Ltac";"Batch";"Debug"];
+      optread  = (fun () -> !batch);
+      optwrite = (fun x -> batch := x) }
+
 let rec drop_spaces inst i =
   if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
   else i
@@ -150,6 +163,7 @@ let rec prompt level =
   begin
     let open Proofview.NonLogical in
     Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+    if Pervasives.(!batch) then return (DebugOn (level+1)) else
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
       begin function (e, info) -> match e with
-- 
cgit v1.2.3


From 6532ee2d63c6e96b930895b0d42c8d9c7cc9e911 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 9 May 2017 00:26:56 +0200
Subject: Prevent user-defined ring morphisms from ever being evaluated.

---
 plugins/setoid_ring/newring.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index d59ffee546..6b8ef630a2 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -333,12 +333,12 @@ let _ = add_map "ring"
     my_reference "gen_phiZ", (function _->Eval);
     (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
-    pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
+    pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
           (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
-    (* PEeval: evaluate morphism and polynomial, protect ring
+    (* PEeval: evaluate polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)])
+    pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot)])
 
 (****************************************************************************)
 (* Ring database *)
@@ -780,20 +780,20 @@ let _ = add_map "field"
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
     my_reference "display_linear",
-      (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
+      (function -1|9|10|11|13|15|16->Eval|12|14->Rec|_->Prot);
     my_reference "display_pow_linear",
      (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot);
    (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
-    pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
+    pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
-          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
-    (* PEeval: evaluate morphism and polynomial, protect ring
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
+    (* PEeval: evaluate polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot);
-    (* FEeval: evaluate morphism, protect field
+    pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot);
+    (* FEeval: evaluate polynomial, protect field
        operations and make recursive call on the var map *)
-    my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);;
+    my_reference "FEeval", (function -1|12|15->Eval|10|14->Rec|_->Prot)]);;
 
 let _ = add_map "field_cond"
   (map_without_eq
-- 
cgit v1.2.3


From e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Apr 2017 21:09:05 +0200
Subject: Typo in a comment of plugin Quote.

---
 plugins/quote/quote.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index fc9d70ae7d..c649cfb2c6 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -8,7 +8,7 @@
 
 (* The `Quote' tactic *)
 
-(* The basic idea is to automatize the inversion of interpetation functions
+(* The basic idea is to automatize the inversion of interpretation functions
    in 2-level approach
 
    Examples are given in \texttt{theories/DEMOS/DemoQuote.v}
-- 
cgit v1.2.3


From cd3971e53b76cb62e14822eb3e275d3968a4f215 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:30:09 +0200
Subject: Adding support for using grammar entries returning no value in
 EXTEND.

---
 plugins/ltac/g_ltac.ml4     |  8 ++++++--
 plugins/ltac/pptactic.ml    |  7 ++++---
 plugins/ltac/pptactic.mli   |  2 +-
 plugins/ltac/tacentries.ml  | 14 +++++++-------
 plugins/ltac/tacentries.mli |  2 +-
 5 files changed, 19 insertions(+), 14 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ca5d198c23..d717ed0a53 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -460,7 +460,9 @@ END
 
 let pr_ltac_production_item = function
 | Tacentries.TacTerm s -> quote (str s)
-| Tacentries.TacNonTerm (_, (arg, sep), id) ->
+| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg
+| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false
+| Tacentries.TacNonTerm (_, (arg, sep), Some id) ->
   let sep = match sep with
   | None -> mt ()
   | Some sep -> str "," ++ spc () ++ quote (str sep)
@@ -470,7 +472,9 @@ let pr_ltac_production_item = function
 VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
 | [ string(s) ] -> [ Tacentries.TacTerm s ]
 | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
-  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ]
+  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ]
+| [ ident(nt) ] ->
+  [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ]
 END
 
 VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b73b66e56f..a619575591 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
 
@@ -264,8 +264,9 @@ type 'a extra_genarg_printer =
       let rec pack prods args = match prods, args with
       | [], [] -> []
       | TacTerm s :: prods, args -> TacTerm s :: pack prods args
-      | TacNonTerm (loc, symb, id) :: prods, arg :: args ->
-        TacNonTerm (loc, (symb, arg), id) :: pack prods args
+      | TacNonTerm (_, _, None) :: prods, args -> pack prods args
+      | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args ->
+        TacNonTerm (loc, (symb, arg), ido) :: pack prods args
       | _ -> raise Not_found
       in
       let prods = pack pp.pptac_prods l in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 729338fb9a..433f342c4f 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -21,7 +21,7 @@ open Ppextend
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 32750383b8..91262f6fd6 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -21,7 +21,7 @@ open Nameops
 
 type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type raw_argument = string * string option
 type argument = Genarg.ArgT.any Extend.user_symbol
@@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let map = function
   | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, s, _) ->
+  | TacNonTerm (loc, s, ido) ->
     let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
-    GramNonTerminal (loc, typ, e)
+    GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e)
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
@@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry =
 
 let interp_prod_item = function
   | TacTerm s -> TacTerm s
-  | TacNonTerm (loc, (nt, sep), id) ->
+  | TacNonTerm (loc, (nt, sep), ido) ->
     let symbol = parse_user_entry nt sep in
     let interp s = function
     | None ->
@@ -220,7 +220,7 @@ let interp_prod_item = function
       end
     in
     let symbol = interp_entry_name interp symbol in
-    TacNonTerm (loc, symbol, id)
+    TacNonTerm (loc, symbol, ido)
 
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
 
 let cons_production_parameter = function
 | TacTerm _ -> None
-| TacNonTerm (_, _, id) -> Some id
+| TacNonTerm (_, _, ido) -> ido
 
 let add_glob_tactic_notation local ~level prods forml ids tac =
   let parule = {
@@ -362,7 +362,7 @@ let add_ml_tactic_notation name ~level prods =
     let open Tacexpr in
     let get_id = function
     | TacTerm s -> None
-    | TacNonTerm (_, _, id) -> Some id
+    | TacNonTerm (_, _, ido) -> ido
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 0695044736..dac62dad33 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
 
 type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
 
 type raw_argument = string * string option
 (** An argument type as provided in Tactic notations, i.e. a string like
-- 
cgit v1.2.3


From b82f27726f5ae891689e3b958323c2a61d4c154b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:31:08 +0200
Subject: Fixing grammar for "evar" by exporting the test_lpar_id_colon trick
 to EXTEND.

---
 plugins/ltac/extraargs.ml4    | 20 ++++++++++++++++++++
 plugins/ltac/extraargs.mli    |  4 ++++
 plugins/ltac/extratactics.ml4 |  2 +-
 plugins/ltac/g_tactic.ml4     | 13 +------------
 4 files changed, 26 insertions(+), 13 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 53b726432c..ec3a49df49 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -274,6 +274,26 @@ ARGUMENT EXTEND in_clause
 | [ in_clause'(cl) ] -> [ cl ]
 END
 
+let local_test_lpar_id_colon =
+  let err () = raise Stream.Failure in
+  Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+    (fun strm ->
+      match Util.stream_nth 0 strm with
+        | Tok.KEYWORD "(" ->
+            (match Util.stream_nth 1 strm with
+              | Tok.IDENT _ ->
+                  (match Util.stream_nth 2 strm with
+                    | Tok.KEYWORD ":" -> ()
+                    | _ -> err ())
+              | _ -> err ())
+        | _ -> err ())
+
+let pr_lpar_id_colon _ _ _ _ = mt ()
+
+ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
+| [ local_test_lpar_id_colon(x) ] -> [ () ]
+END
+
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
 let pr_r_nat_field natf =
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 7d4bccfadd..9b41675120 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,6 +67,10 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
+val test_lpar_id_colon : unit Pcoq.Gram.entry
+
+val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
+
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 3e6ccaf84a..bd48614dbc 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -463,7 +463,7 @@ open Evar_tactics
 (* TODO: add support for some test similar to g_constr.name_colon so that
    expressions like "evar (list A)" do not raise a syntax error *)
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 4b3ca80af5..e33c25cf88 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -72,18 +72,7 @@ let test_lpar_idnum_coloneq =
         | _ -> err ())
 
 (* idem for (x:t) *)
-let test_lpar_id_colon =
-  Gram.Entry.of_parser "lpar_id_colon"
-    (fun strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
-- 
cgit v1.2.3


From 79595b45e68c6234aff54f076687a8024c4a2aaa Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 18 May 2017 12:50:36 -0400
Subject: Add .dir-locals.el to plugins

As requested in
https://github.com/coq/coq/pull/386#issuecomment-302358542
---
 plugins/.dir-locals.el | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 plugins/.dir-locals.el

(limited to 'plugins')

diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el
new file mode 100644
index 0000000000..4e8830f6c1
--- /dev/null
+++ b/plugins/.dir-locals.el
@@ -0,0 +1,4 @@
+((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
+						buffer-file-name ".dir-locals.el")))
+			(setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq"))
+			(setq-local coq-prog-name (expand-file-name "../bin/coqtop")))))))
-- 
cgit v1.2.3