From d272cd02ef9ba2509c266f58ee39f51106ae53c2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/firstorder/rules.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index a60fd4d8f..96601f74a 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)])
-- 
cgit v1.2.3


From a1fd5fb489237a1300adb242e2c9b6c74c82981b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 7773f6a2f..ade94e98e 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 5db8ff59a..3f438c04a 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 3c0319319..8ef6a09d0 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 d6cd7e2a0..ab1dd07c1 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 b5669463c..4fd1e38a2 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 9dc2a51a6..62f811546 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 ce711f3f9..47550f314 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 96601f74a..e0d2c38a7 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 381b7cd87..80a7ae2c2 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 fb0c22c2b..59b842c82 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 06c9251e7..18d68f54f 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 7cbfb8e7d..49bf07155 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 4fe9ad38d..c9cca9bd8 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 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 dev/top_printers.ml                             |  1 -
 engine/eConstr.ml                               |  1 -
 engine/eConstr.mli                              |  1 -
 engine/evarutil.ml                              |  1 -
 engine/evd.ml                                   |  4 ----
 engine/proofview.mli                            |  1 -
 engine/termops.ml                               |  1 -
 engine/universes.ml                             |  1 -
 interp/constrintern.ml                          |  2 --
 interp/constrintern.mli                         |  1 -
 interp/stdarg.ml                                |  2 --
 interp/stdarg.mli                               |  1 -
 interp/syntax_def.ml                            |  2 --
 intf/tactypes.mli                               |  1 -
 library/goptions.ml                             |  1 -
 library/libobject.ml                            |  1 -
 parsing/egramcoq.ml                             |  1 -
 parsing/egramcoq.mli                            |  8 --------
 parsing/g_prim.ml4                              |  1 -
 parsing/g_proofs.ml4                            |  1 -
 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 -
 pretyping/cbv.mli                               |  1 -
 pretyping/classops.ml                           |  1 -
 pretyping/classops.mli                          |  1 -
 pretyping/coercion.ml                           |  1 -
 pretyping/coercion.mli                          |  1 -
 pretyping/detyping.ml                           |  1 -
 pretyping/evarconv.ml                           |  1 -
 pretyping/evarconv.mli                          |  1 -
 pretyping/evardefine.ml                         |  1 -
 pretyping/find_subterm.mli                      |  1 -
 pretyping/inductiveops.ml                       |  1 -
 pretyping/patternops.ml                         |  1 -
 pretyping/patternops.mli                        |  1 -
 pretyping/pretype_errors.ml                     |  1 -
 pretyping/pretyping.ml                          |  1 -
 pretyping/program.ml                            |  1 -
 pretyping/tacred.mli                            |  1 -
 pretyping/typeclasses_errors.ml                 |  1 -
 pretyping/typeclasses_errors.mli                |  1 -
 printing/prettyp.mli                            |  1 -
 proofs/clenvtac.mli                             |  1 -
 proofs/goal.ml                                  |  1 -
 proofs/proof_type.mli                           |  3 ---
 proofs/refiner.ml                               |  1 -
 proofs/tacmach.mli                              |  1 -
 stm/stm.mli                                     |  3 ---
 tactics/auto.ml                                 |  1 -
 tactics/auto.mli                                |  1 -
 tactics/btermdn.mli                             |  1 -
 tactics/class_tactics.ml                        |  3 ---
 tactics/class_tactics.mli                       |  1 -
 tactics/contradiction.mli                       |  1 -
 tactics/eauto.mli                               |  2 --
 tactics/elim.ml                                 |  1 -
 tactics/elim.mli                                |  1 -
 tactics/eqdecide.ml                             |  1 -
 tactics/equality.ml                             |  1 -
 tactics/equality.mli                            |  1 -
 tactics/hints.mli                               |  1 -
 tactics/hipattern.mli                           |  1 -
 tactics/inv.ml                                  |  1 -
 tactics/inv.mli                                 |  1 -
 tactics/leminv.mli                              |  1 -
 tactics/tactics.ml                              |  2 --
 toplevel/coqloop.mli                            |  2 --
 vernac/auto_ind_decl.ml                         |  2 --
 vernac/classes.ml                               |  2 --
 vernac/obligations.mli                          |  1 -
 vernac/search.ml                                |  2 --
 vernac/search.mli                               |  1 -
 94 files changed, 137 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 918e98f77..7caaf2d9d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -503,7 +503,6 @@ VERNAC COMMAND EXTEND PrintConstr
 END
 *)
 
-open Pcoq
 open Genarg
 open Stdarg
 open Egramml
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bb9075e74..54d3ce6cf 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open CSig
 open CErrors
 open Util
 open Names
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 3a9469e55..693b592fd 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -9,7 +9,6 @@
 open CSig
 open Names
 open Constr
-open Context
 open Environ
 
 type t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 1624dc93e..fba466107 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Names
 open Term
-open Vars
 open Termops
 open Namegen
 open Pre_env
diff --git a/engine/evd.ml b/engine/evd.ml
index 5419a10a8..6b1e1a855 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -14,8 +14,6 @@ open Nameops
 open Term
 open Vars
 open Environ
-open Globnames
-open Context.Named.Declaration
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
@@ -360,8 +358,6 @@ module EvMap = Evar.Map
 module EvNames :
 sig
 
-open Misctypes
-
 type t
 
 val empty : t
diff --git a/engine/proofview.mli b/engine/proofview.mli
index a3b0304b1..da8a8fecd 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -13,7 +13,6 @@
     state and returning a value of type ['a]. *)
 
 open Util
-open Term
 open EConstr
 
 (** Main state of tactics *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 29dcddbb0..19e62f8e6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1427,7 +1427,6 @@ let dependency_closure env sigma sign hyps =
     List.rev lh
 
 let global_app_of_constr sigma c =
-  let open Univ in
   let open Globnames in
   match EConstr.kind sigma c with
   | Const (c, u) -> (ConstRef c, u), None
diff --git a/engine/universes.ml b/engine/universes.ml
index ab561784c..1900112dd 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -13,7 +13,6 @@ open Term
 open Environ
 open Univ
 open Globnames
-open Decl_kinds
 
 let pr_with_global_universes l = 
   try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ())))
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d75487ecf..389880c5c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2045,8 +2045,6 @@ let interp_binder_evars env evdref na t =
   let t' = locate_if_hole (loc_of_glob_constr t) na t in
   understand_tcc_evars env evdref ~expected_type:IsType t'
 
-open Environ
-
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 758d4e650..fdd50c6a1 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -18,7 +18,6 @@ open Constrexpr
 open Notation_term
 open Pretyping
 open Misctypes
-open Decl_kinds
 
 (** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
 
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 341ff5662..5920b0d50 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Misctypes
-open Tactypes
 open Genarg
 open Geninterp
 
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 113fe40ba..ac40a2328 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -10,7 +10,6 @@
 
 open Loc
 open Names
-open Term
 open EConstr
 open Libnames
 open Globnames
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index c3f4c4f30..ed7b0b70d 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -106,5 +106,3 @@ let search_syntactic_definition kn =
   let def = out_pat pat in
   verbose_compat kn def v;
   def
-
-open Goptions
diff --git a/intf/tactypes.mli b/intf/tactypes.mli
index 02cfc44e2..ef90b911c 100644
--- a/intf/tactypes.mli
+++ b/intf/tactypes.mli
@@ -13,7 +13,6 @@
 open Loc
 open Names
 open Constrexpr
-open Glob_term
 open Pattern
 open Misctypes
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 1c08b9539..c111113ca 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -235,7 +235,6 @@ with Not_found ->
   then error "Sorry, this option name is already used."
 
 open Libobject
-open Lib
 
 let warn_deprecated_option =
   CWarnings.create ~name:"deprecated-option" ~category:"deprecated"
diff --git a/library/libobject.ml b/library/libobject.ml
index 8757ca08c..897591762 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -8,7 +8,6 @@
 
 open Libnames
 open Pp
-open Util
 
 module Dyn = Dyn.Make(struct end)
 
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 65e99d1b9..86c66ec5f 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Pcoq
 open Constrexpr
-open Notation
 open Notation_term
 open Extend
 open Libnames
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 6dda3817a..0a0430ba6 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -6,14 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Constrexpr
-open Notation_term
-open Pcoq
-open Extend
-open Genarg
-open Egramml
-
 (** Mapping of grammar productions to camlp4 actions *)
 
 (** This is the part specific to Coq-level Notation and Tactic Notation.
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 2af4ed533..abb463f82 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -8,7 +8,6 @@
 
 open Names
 open Libnames
-open Tok (* necessary for camlp4 *)
 
 open Pcoq
 open Pcoq.Prim
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 7ca2e4a4f..68b8be6b8 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -9,7 +9,6 @@
 open Constrexpr
 open Vernacexpr
 open Misctypes
-open Tok
 
 open Pcoq
 open Pcoq.Prim
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 62f811546..2b624b983 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 7ddc84d01..61752aa33 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 0dccd25d7..b5eacee81 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 7b0d7d27d..c6f5c2745 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 94ec0a898..29472cdef 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 f1ca57585..0af0898a0 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 5d3f6df03..bc9c300e2 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 35cfe8b54..21419d1f9 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 dfa8331ff..50e8255a6 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 ff5e7d5ff..23ce368ee 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 1d21118ae..7e979d269 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 7a20838a2..6683d753b 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 9c4ac5265..4a44f86d9 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 ef1d69d35..32750383b 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 94e14223a..d1e2a7bbe 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 fcdf7bb2c..b8c021f18 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 1e5f6bd42..494f36a95 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 7745d9b7b..0b4d35a22 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 eb26c5431..a36607ec3 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 41f2edfcf..a120d4efb 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 6e072e831..d59ffee54 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 4367d021c..d9d32c681 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 f146fbb11..72c70750c 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 1f984b160..638b4e254 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
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index b014af2c7..eb25994be 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Environ
 open CClosure
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index e9b3d197b..32da81f96 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -17,7 +17,6 @@ open Nametab
 open Environ
 open Libobject
 open Term
-open Termops
 open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 0d741a5a5..c4238e8b0 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open EConstr
 open Evd
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 542db7fdf..c26e7458e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -22,7 +22,6 @@ open Environ
 open EConstr
 open Vars
 open Reductionops
-open Typeops
 open Pretype_errors
 open Classops
 open Evarutil
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index bc63d092d..ea3d3f0fa 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -8,7 +8,6 @@
 
 open Evd
 open Names
-open Term
 open Environ
 open EConstr
 open Glob_term
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8ba408679..483e2b432 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -13,7 +13,6 @@ open CErrors
 open Util
 open Names
 open Term
-open Environ
 open EConstr
 open Vars
 open Inductiveops
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4bb66b8e9..305eae15a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -21,7 +21,6 @@ open Recordops
 open Evarutil
 open Evardefine
 open Evarsolve
-open Globnames
 open Evd
 open Pretype_errors
 open Sigma.Notations
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index fc07f0fbe..7cee1e8a7 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Environ
 open Reductionops
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index c5ae684e3..5fd104c78 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -11,7 +11,6 @@ open Pp
 open Names
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index e3d3b74f1..d22f94e4e 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Locus
-open Term
 open Evd
 open Pretype_errors
 open Environ
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5b42add28..429e5005e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -459,7 +459,6 @@ let extract_mrectype sigma t =
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
-  let open EConstr in
   let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b16d04495..33a68589c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -20,7 +20,6 @@ open Mod_subst
 open Misctypes
 open Decl_kinds
 open Pattern
-open Evd
 open Environ
 
 let case_info_pattern_eq i1 i2 =
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 5694d345c..791fd74ed 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Globnames
 open Glob_term
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 24f6d1689..f9cf6b83b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Term
 open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 497bde340..68ef97659 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -33,7 +33,6 @@ open EConstr
 open Vars
 open Reductionops
 open Type_errors
-open Typeops
 open Typing
 open Globnames
 open Nameops
diff --git a/pretyping/program.ml b/pretyping/program.ml
index caa5a5c8a..42acc5705 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 76d0bc241..c31212e26 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open Evd
 open EConstr
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 2db0e9e88..754dacd19 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Term
 open EConstr
 open Environ
 open Constrexpr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 9bd430e4d..558575ccc 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -8,7 +8,6 @@
 
 open Loc
 open Names
-open Term
 open EConstr
 open Environ
 open Constrexpr
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 38e111034..6841781cc 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -8,7 +8,6 @@
 
 open Pp
 open Names
-open Term
 open Environ
 open Reductionops
 open Libnames
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 5b7164705..26069207e 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -8,7 +8,6 @@
 
 (** Legacy components of the previous proof engine. *)
 
-open Term
 open Clenv
 open EConstr
 open Unification
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 9046f4534..fc8e635a0 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Pp
-open Term
 open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 03bc5e471..e59db9e42 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,9 +11,6 @@
 open Evd
 open Names
 open Term
-open Glob_term
-open Nametab
-open Misctypes
 
 (** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index bc12b3ba7..259e96a27 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Evd
-open Environ
 open Proof_type
 open Logic
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 627a8e0e7..e6e60e27f 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -15,7 +15,6 @@ open Proof_type
 open Redexpr
 open Pattern
 open Locus
-open Misctypes
 
 (** Operations for handling terms under a local typing context. *)
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 30e9629c6..d2bee4496 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -6,10 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Vernacexpr
 open Names
-open Feedback
-open Loc
 
 (** state-transaction-machine interface *)
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 42230dff1..324c551d0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open CErrors
 open Names
-open Vars
 open Termops
 open EConstr
 open Environ
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 32710e347..9ed9f0ae2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -9,7 +9,6 @@
 (** This files implements auto and related automation tactics *)
 
 open Names
-open Term
 open EConstr
 open Clenv
 open Pattern
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 2a5e7c345..27f624f71 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Pattern
 open Names
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c430e776a..6c724a1eb 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -18,7 +18,6 @@ open Names
 open Term
 open Termops
 open EConstr
-open Reduction
 open Proof_type
 open Tacticals
 open Tacmach
@@ -1219,7 +1218,6 @@ module Search = struct
 
   let intro_tac info kont gl =
     let open Proofview in
-    let open Proofview.Notations in
     let env = Goal.env gl in
     let sigma = Goal.sigma gl in
     let s = Sigma.to_evar_map sigma in
@@ -1257,7 +1255,6 @@ module Search = struct
   let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
         unit Proofview.tactic =
     let open Proofview in
-    let open Proofview.Notations in
     if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
       Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
     else
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 738cc0feb..4ab29f260 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -9,7 +9,6 @@
 (** This files implements typeclasses eauto *)
 
 open Names
-open Constr
 open EConstr
 open Tacmach
 
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 510b135b0..2cf5a6829 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Misctypes
 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e2006ac1e..c952f4e72 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
-open Proof_type
 open Hints
 open Tactypes
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index e37ec6bce..855cb206f 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Names
-open Term
 open Termops
 open EConstr
 open Inductiveops
diff --git a/tactics/elim.mli b/tactics/elim.mli
index dc1af79ba..fb7cc7b83 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Tacticals
 open Misctypes
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bac3980d2..5012b0ef7 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -25,7 +25,6 @@ open Constr_matching
 open Misctypes
 open Tactypes
 open Hipattern
-open Pretyping
 open Proofview.Notations
 open Tacmach.New
 open Coqlib
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 25c28cf4a..cc7701ad5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -14,7 +14,6 @@ open Names
 open Nameops
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 5467b4af2..d979c580a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Term
 open Evd
 open EConstr
 open Environ
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 467fd46d5..3a0339ff5 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -9,7 +9,6 @@
 open Pp
 open Util
 open Names
-open Term
 open EConstr
 open Environ
 open Globnames
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index dd09c3a4d..82a3d47b5 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Evd
 open EConstr
 open Coqlib
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 904a17417..266cac5c7 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 446a62f6d..5835e763d 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Misctypes
 open Tactypes
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 26d4ac994..a343fc81a 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Constrexpr
 open Misctypes
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 53f8e4d5f..f3f7d16b7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5037,8 +5037,6 @@ end
 
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
-  open Proofview.Notations
-
   open Genredexpr
   open Locus
 
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 66bbf43f6..13e860a88 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-
 (** The Coq toplevel loop. *)
 
 (** A buffer for the character read from a channel. We store the command
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 015552d68..25091f783 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -9,7 +9,6 @@
 (* This file is about the automatic generation of schemes about
    decidable equality, created by Vincent Siles, Oct 2007 *)
 
-open Tacmach
 open CErrors
 open Util
 open Pp
@@ -716,7 +715,6 @@ let compute_lb_goal ind lnamesparrec nparrec =
         ))), eff
 
 let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
-  let open EConstr in
   let list_id = list_id lnamesparrec in
     let avoid = ref [] in
       let first_intros =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 833719965..d515b0c9b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -66,8 +66,6 @@ let _ =
   Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
 
-open Vernacexpr
-
 (** TODO: add subinstances *)
 let existing_instance glob g info =
   let c = global g in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 11366fe91..a276f9f9a 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -12,7 +12,6 @@ open Evd
 open Names
 open Pp
 open Globnames
-open Vernacexpr
 open Decl_kinds
 
 (** Forward declaration. *)
diff --git a/vernac/search.ml b/vernac/search.ml
index 6279b17ae..5b6e9a9c3 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -14,11 +14,9 @@ open Declarations
 open Libobject
 open Environ
 open Pattern
-open Printer
 open Libnames
 open Globnames
 open Nametab
-open Goptions
 
 module NamedDecl = Context.Named.Declaration
 
diff --git a/vernac/search.mli b/vernac/search.mli
index 82b79f75d..e34522d8a 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open Environ
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 engine/evd.ml                                  |  2 +-
 interp/notation.ml                             |  1 -
 kernel/constr.ml                               | 22 ----------------------
 lib/cErrors.ml                                 |  2 ++
 parsing/pcoq.ml                                |  1 -
 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 ++++++----
 pretyping/evarsolve.ml                         |  1 -
 pretyping/reductionops.ml                      |  6 +++++-
 pretyping/reductionops.mli                     |  5 ++++-
 pretyping/unification.ml                       |  2 +-
 printing/prettyp.ml                            |  2 +-
 stm/stm.ml                                     |  3 +++
 stm/vcs.ml                                     |  2 --
 tools/coqwc.mll                                |  2 ++
 21 files changed, 40 insertions(+), 54 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/engine/evd.ml b/engine/evd.ml
index 6b1e1a855..db048bbd6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -15,7 +15,7 @@ open Term
 open Vars
 open Environ
 
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
 (** Generic filters *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 90ac7f729..6aa6f54c0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -22,7 +22,6 @@ open Glob_ops
 open Ppextend
 open Context.Named.Declaration
 
-module NamedDecl = Context.Named.Declaration
 (*i*)
 
 (*s A scope is a set of notations; it includes
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 5a7561bf5..71efe9032 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -978,28 +978,6 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash)
 
 let case_info_hash = CaseinfoHash.hash
 
-module Hsorts =
-  Hashcons.Make(
-    struct
-      open Sorts
-
-      type t = Sorts.t
-      type u = universe -> universe
-      let hashcons huniv = function
-          Prop c -> Prop c
-        | Type u -> Type (huniv u)
-      let eq s1 s2 =
-        s1 == s2 ||
-	  match (s1,s2) with
-            (Prop c1, Prop c2) -> c1 == c2
-          | (Type u1, Type u2) -> u1 == u2
-          |_ -> false
-      let hash = function
-	| Prop Null -> 0 | Prop Pos -> 1
-	| Type u -> 2 + Universe.hash u
-    end)
-
-(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
 let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind
 
 let hcons =
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 1c1ff7e2f..b55fd80c6 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -121,12 +121,14 @@ end
     by inner functions during a [vernacinterp]. They should be handled
     only at the very end of interp, to be displayed to the user. *)
 
+[@@@ocaml.warning "-52"]
 let noncritical = function
   | Sys.Break | Out_of_memory | Stack_overflow
   | Assert_failure _ | Match_failure _ | Anomaly _
   | Timeout | Drop | Quit -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
+[@@@ocaml.warning "+52"]
 
 (** Check whether an exception is handled *)
 
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 3f014c4c8..9a4766c0b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open CErrors
 open Util
 open Extend
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 8ef6a09d0..b25017535 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 df81bc78c..55d361e3d 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 c6f5c2745..848b44a60 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 29472cdef..6c0c28905 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 1e405d2c9..bd30f1159 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 12a1566e2..9a1615d3f 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 e86d1c728..4de2081cf 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 bd991a955..334b03de1 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;
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 77086d046..f0d011477 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
 open Util
 open CErrors
 open Names
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index da3add2e5..52f424f75 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -239,6 +239,9 @@ sig
   | Shift of int
   | Update of 'a
   and 'a t = 'a member list
+
+  exception IncompatibleFold2
+
   val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
   val empty : 'a t
   val is_empty : 'a t -> bool
@@ -413,6 +416,7 @@ struct
       | (_,_) -> false in
     compare_rec 0 stk1 stk2
 
+  exception IncompatibleFold2
   let fold2 f o sk1 sk2 =
     let rec aux o lft1 sk1 lft2 sk2 =
       let fold_array =
@@ -442,7 +446,7 @@ struct
 	  aux o lft1 (List.rev params1) lft2 (List.rev params2)
 	in aux o' lft1' q1 lft2' q2
       | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
-	raise (Invalid_argument "Reductionops.Stack.fold2")
+	raise IncompatibleFold2
     in aux o 0 (List.rev sk1) 0 (List.rev sk2)
 
   let rec map f x = List.map (function
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 752c30a8a..af8048156 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -81,8 +81,11 @@ module Stack : sig
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
 
   val compare_shape : 'a t -> 'a t -> bool
+
+  exception IncompatibleFold2
   (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
-      @return the result and the lifts to apply on the terms *)
+      @return the result and the lifts to apply on the terms
+      @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *)
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
     constr t -> constr t -> 'a * int * int
   val map : ('a -> 'a) -> 'a t -> 'a t
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4a3836d86..661c1d865 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1095,7 +1095,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       let app = mkApp (c, Array.rev_of_list ks) in
       (* let substn = unirec_rec curenvnb pb b false substn t cN in *)
 	unirec_rec curenvnb pb opt' substn c1 app
-      with Invalid_argument "Reductionops.Stack.fold2" ->
+      with Reductionops.Stack.IncompatibleFold2 ->
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
   in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index aa422e36a..381af83c7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -29,7 +29,7 @@ open Printer
 open Printmod
 open Context.Rel.Declaration
 
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
diff --git a/stm/stm.ml b/stm/stm.ml
index 8c1185b6d..84c8aa9a9 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1205,6 +1205,8 @@ let detect_proof_block id name =
 (****************************** THE SCHEDULER *********************************)
 (******************************************************************************)
 
+(* Unused module warning doesn't understand [module rec] *)
+[@@@ocaml.warning "-60"]
 module rec ProofTask : sig
  
   type competence = Stateid.t list
@@ -2318,6 +2320,7 @@ let known_state ?(redefine_qed=false) ~cache id =
   reach ~redefine_qed id
 
 end (* }}} *)
+[@@@ocaml.warning "+60"]
 
 (********************************* STM API ************************************)
 (******************************************************************************)
diff --git a/stm/vcs.ml b/stm/vcs.ml
index d3886464d..88f860eb6 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -74,8 +74,6 @@ module Dag = Dag.Make(OT)
 
 type id = OT.t
 
-module NodeSet = Dag.NodeSet
-
 module Branch =
 struct
   type t = string
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index b4fc738d0..cd07d4216 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -239,6 +239,7 @@ let process_channel ch =
   if !skip_header then read_header lb;
   spec lb
 
+[@@@ocaml.warning "-52"]
 let process_file f =
   try
     let ch = open_in f in
@@ -251,6 +252,7 @@ let process_file f =
 	flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
     | Sys_error s ->
 	flush stdout; eprintf "coqwc: %s\n" s; flush stderr
+[@@@ocaml.warning "+52"]
 
 (*s Parsing of the command line. *)
 
-- 
cgit v1.2.3


From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
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 -
 pretyping/constr_matching.ml    | 1 -
 tactics/auto.ml                 | 3 ---
 tactics/class_tactics.ml        | 1 -
 tactics/class_tactics.mli       | 1 -
 vernac/topfmt.ml                | 1 -
 15 files changed, 19 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 00b31ccce..7c5efaea3 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 5099d847b..b4bb62be8 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 ade94e98e..9900792ca 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 2b624b983..5a1e7c26a 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 e0d2c38a7..86a677007 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 80a7ae2c2..fb2173083 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 59b842c82..2d18b6605 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 18d68f54f..6ed251f34 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 fdcaedab3..ac979bcf8 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 9a1615d3f..5630a2d7b 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
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index d55350622..2334be966 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -87,7 +87,6 @@ let rec build_lambda sigma vars ctx m = match vars with
 | n :: vars ->
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
-  let len = List.length ctx in
   let pre, suf = List.chop (pred n) ctx in
   let (na, t, suf) = match suf with
   | [] -> assert false
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 324c551d0..c2d12ebd0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,15 +10,12 @@ module CVars = Vars
 
 open Pp
 open Util
-open CErrors
 open Names
 open Termops
 open EConstr
 open Environ
-open Tacmach
 open Genredexpr
 open Tactics
-open Tacticals
 open Clenv
 open Locus
 open Proofview.Notations
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6c724a1eb..2d6dffdd2 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -19,7 +19,6 @@ open Term
 open Termops
 open EConstr
 open Proof_type
-open Tacticals
 open Tacmach
 open Tactics
 open Clenv
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 4ab29f260..c5731e377 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -10,7 +10,6 @@
 
 open Names
 open EConstr
-open Tacmach
 
 val catchable : exn -> bool
 
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index e44b585d7..6d9d71a62 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -131,7 +131,6 @@ let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
 let info_hdr = mt ()
 let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
 let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
-let  ann_hdr = tag Tag.error   (str "Anomaly:") ++ spc ()
 
 let make_body quoter info ?pre_hdr s =
   pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s))
-- 
cgit v1.2.3