1 files changed, 112 insertions, 80 deletions

diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index ffb63af0..cfcd6561 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -1,25 +1,31 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 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
 open Sequent
 open Globnames
 open Locus
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
+
+type tactic = unit Proofview.tactic
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
@@ -27,136 +33,157 @@ 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 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")
+	  []->anomaly (Pp.str "Not the expected number of hyps.")
 	| nd::q->
-            let id = get_id nd in
-	    if occur_var env id (pf_concl gls) ||
-	      List.exists (occur_var_in_decl env id) ctx then
+            let id = NamedDecl.get_id nd in
+	    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) (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 (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 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 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 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 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
-         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 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 cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d idc =mkLambda (Anonymous,b,
+  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
 
@@ -164,37 +191,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 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 prod))
+    (tclTHENS (cut prod)
        [tclTHENLIST
-	  [Proofview.V82.of_tactic intro;
-           pf_constr_of_global id (fun idc ->
-	   (fun gls->
-	      let id0=pf_nth_hyp_id gls 1 in
+	  [intro;
+           (pf_constr_of_global id >>= fun idc ->
+	   Proofview.Goal.enter begin fun gls->
+              let open EConstr 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
@@ -203,15 +233,17 @@ let ll_forall_tac prod backtrack id continue seq=
 
 (* special for compatibility with old Intuition *)
 
-let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+let constant str = Universes.constr_of_global
+  @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [AllOccurrences,EvalConstRef (fst (destConst (constant "not")));
-   AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))]
+  [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not")));
+   AllOccurrences,EvalConstRef (fst (Constr.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 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