From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 plugins/rtauto/refl_tauto.ml | 72 ++++++++++++++++++++++++--------------------
 1 file changed, 39 insertions(+), 33 deletions(-)

(limited to 'plugins/rtauto/refl_tauto.ml')

diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 4ed90795..946b6dff 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -1,16 +1,21 @@
 (************************************************************************)
-(*  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)         *)
 (************************************************************************)
 
+
 module Search = Explore.Make(Proof_search)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Term
+open Constr
 open Tacmach
 open Proof_search
 open Context.Named.Declaration
@@ -21,28 +26,28 @@ let step_count = ref 0
 
 let node_count = ref 0
 
-let logic_constant =
-  Coqlib.gen_constant "refl_tauto" ["Init";"Logic"]
+let logic_constant s = Universes.constr_of_global @@
+  Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s
 
 let li_False = lazy (destInd (logic_constant "False"))
-let li_and = lazy (destInd (logic_constant "and"))
-let li_or =  lazy (destInd (logic_constant "or"))
+let li_and   = lazy (destInd (logic_constant "and"))
+let li_or    = lazy (destInd (logic_constant "or"))
 
-let pos_constant =
-  Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"]
+let pos_constant s = Universes.constr_of_global @@
+  Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s
 
 let l_xI = lazy (pos_constant "xI")
 let l_xO = lazy (pos_constant "xO")
 let l_xH = lazy (pos_constant "xH")
 
-let store_constant =
-  Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"]
+let store_constant s = Universes.constr_of_global @@
+  Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s
 
 let l_empty = lazy (store_constant "empty")
 let l_push = lazy (store_constant "push")
 
-let constant=
-  Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"]
+let constant s = Universes.constr_of_global @@
+  Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s
 
 let l_Reflect = lazy (constant "Reflect")
 
@@ -66,22 +71,21 @@ let l_E_Or = lazy (constant "E_Or")
 let l_D_Or = lazy (constant "D_Or")
 
 
-let special_whd gl=
-  let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let special_whd gl c =
+  Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c
 
-let special_nf gl=
-  let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
-    (fun t -> CClosure.norm_val infos (CClosure.inject t))
+let special_nf gl c =
+  Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c
 
 type atom_env=
     {mutable next:int;
      mutable env:(constr*int) list}
 
 let make_atom atom_env term=
+  let term = EConstr.Unsafe.to_constr term in
   try
     let (_,i)=
-      List.find (fun (t,_)-> eq_constr term t) atom_env.env
+      List.find (fun (t,_)-> Constr.equal term t) atom_env.env
     in Atom i
   with Not_found ->
     let i=atom_env.next in
@@ -90,13 +94,16 @@ let make_atom atom_env term=
       Atom i
 
 let rec make_form atom_env gls term =
+  let open EConstr in
+  let open Vars in
   let normalize=special_nf gls in
   let cciterm=special_whd gls term  in
-    match kind_of_term cciterm with
+  let sigma = Tacmach.project gls in
+    match EConstr.kind sigma cciterm with
 	Prod(_,a,b) ->
-	  if not (Termops.dependent (mkRel 1) b) &&
+	  if noccurn sigma 1 b &&
 	    Retyping.get_sort_family_of
-	    (pf_env gls) (Tacmach.project gls) a == InProp
+	    (pf_env gls) sigma a == InProp
 	  then
 	    let fa=make_form atom_env gls a in
 	    let fb=make_form atom_env gls b in
@@ -113,7 +120,7 @@ let rec make_form atom_env gls term =
       | App(hd,argv) when Int.equal (Array.length argv) 2 ->
 	  begin
 	    try
-	      let ind, _ = destInd hd in
+	      let ind, _ = destInd sigma hd in
 		if Names.eq_ind ind (fst (Lazy.force li_and)) then
 		  let fa=make_form atom_env gls argv.(0) in
 		  let fb=make_form atom_env gls argv.(1) in
@@ -134,7 +141,7 @@ let rec make_hyps atom_env gls lenv = function
   | LocalAssum (id,typ)::rest ->
       let hrec=
 	make_hyps atom_env gls (typ::lenv) rest in
-	if List.exists (Termops.dependent (mkVar id)) lenv ||
+	if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv ||
 	  (Retyping.get_sort_family_of
 	     (pf_env gls) (Tacmach.project gls) typ != InProp)
 	then
@@ -233,8 +240,7 @@ open Goptions
 let verbose = ref false
 
 let opt_verbose=
-  {optsync=true;
-   optdepr=false;
+  {optdepr=false;
    optname="Rtauto Verbose";
    optkey=["Rtauto";"Verbose"];
    optread=(fun () -> !verbose);
@@ -245,8 +251,7 @@ let _ = declare_bool_option opt_verbose
 let check = ref false
 
 let opt_check=
-  {optsync=true;
-   optdepr=false;
+  {optdepr=false;
    optname="Rtauto Check";
    optkey=["Rtauto";"Check"];
    optread=(fun () -> !check);
@@ -263,7 +268,7 @@ let rtauto_tac gls=
   let _=
     if Retyping.get_sort_family_of
       (pf_env gls) (Tacmach.project gls) gl != InProp
-    then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
+    then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
   let glf=make_form gamma gls gl in
   let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
   let formula=
@@ -282,7 +287,7 @@ let rtauto_tac gls=
   let prf =
     try project (search_fun (init_state [] formula))
     with Not_found ->
-      errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in
+      user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in
   let search_end_time = System.get_time () in
   let _ = if !verbose then
     begin
@@ -298,7 +303,7 @@ let rtauto_tac gls=
 		      build_form formula;
 		      build_proof [] 0 prf|]) in
   let term=
-    applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+    applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in
   let build_end_time=System.get_time () in
   let _ = if !verbose then
     begin
@@ -312,6 +317,7 @@ let rtauto_tac gls=
 	     str "Giving proof term to Coq ... ")
     end in
   let tac_start_time = System.get_time () in
+  let term = EConstr.of_constr term in
   let result=
     if !check then
       Proofview.V82.of_tactic (Tactics.exact_check term) gls
-- 
cgit v1.2.3