1 files changed, 110 insertions, 58 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f56e9241..a0b9217c 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,8 +1,10 @@
 open Names
 open Pp
+open Constr
 open Libnames
 open Globnames
 open Refiner
+
 let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
 let mk_rel_id = mk_prefix "R_"
 let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
@@ -12,7 +14,7 @@ let mk_equation_id id = Nameops.add_suffix id "_equation"
 let msgnl m =
   ()
 
-let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid)
 
 let fresh_name avoid s = Name (fresh_id avoid s)
 
@@ -21,19 +23,16 @@ 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
   | _ -> raise Not_found
 
 let locate  ref =
-    let (loc,qid) = qualid_of_reference ref in
+    let {CAst.v=qid} = qualid_of_reference ref in
     Nametab.locate qid
 
 let locate_ind ref =
@@ -49,7 +48,7 @@ let locate_constant ref =
 
 let locate_with_msg msg f x =
   try f x
-  with Not_found -> raise (CErrors.UserError("", msg))
+  with Not_found -> raise (CErrors.UserError(None, msg))
 
 
 let filter_map filter f =
@@ -69,11 +68,11 @@ let chop_rlambda_n  =
       if n == 0
       then List.rev acc,rt
       else
-	match rt with
-	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
-	  | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
+	match DAst.get rt with
+	  | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
+	  | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
 	  | _ ->
-	      raise (CErrors.UserError("chop_rlambda_n",
+	      raise (CErrors.UserError(Some "chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
   in
   chop_lambda_n []
@@ -83,9 +82,9 @@ let chop_rprod_n  =
       if n == 0
       then List.rev acc,rt
       else
-	match rt with
-	  | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
-	  | _ -> raise (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+	match DAst.get rt with
+	  | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+	  | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
 
@@ -101,20 +100,15 @@ let list_union_eq eq_fun l1 l2 =
 let list_add_set_eq eq_fun x l =
   if List.exists (eq_fun x) l then l else x::l
 
-
-
-
 let const_of_id id =
-  let _,princ_ref =
-    qualid_of_reference (Libnames.Ident (Loc.ghost,id))
-  in
+  let princ_ref = qualid_of_ident id in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
-    CErrors.errorlabstrm "IndFun.const_of_id"
-      (str "cannot find " ++ Nameops.pr_id id)
+    CErrors.user_err ~hdr:"IndFun.const_of_id"
+      (str "cannot find " ++ Id.print id)
 
 let def_of_const t =
-   match (Term.kind_of_term t) with
+   match Constr.kind t with
     Term.Const sp ->
       (try (match Environ.constant_opt_value_in (Global.env()) sp with
              | Some c -> c
@@ -123,15 +117,16 @@ let def_of_const t =
     |_ -> assert false
 
 let coq_constant s =
-  Coqlib.gen_constant_in_modules "RecursiveDefinition"
+  Universes.constr_of_global @@
+  Coqlib.gen_reference_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
 let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
   Nametab.locate (make_qualid dp (Id.of_string s))
 
-let eq = lazy(coq_constant "eq")
-let refl_equal = lazy(coq_constant "eq_refl")
+let eq = lazy(EConstr.of_constr (coq_constant "eq"))
+let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 
 (*****************************************************************)
 (* Copy of the standart save mechanism but without the much too  *)
@@ -162,7 +157,7 @@ let save with_clean id const (locality,_,kind) hook =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	(locality, ConstRef kn)
   in
-  if with_clean then  Pfedit.delete_current_proof ();
+  if with_clean then Proof_global.discard_current ();
   CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
   definition_message id
 
@@ -174,7 +169,7 @@ let cook_proof _ =
 
 let get_proof_clean do_reduce =
   let result = cook_proof do_reduce in
-  Pfedit.delete_current_proof ();
+  Proof_global.discard_current ();
   result
 
 let with_full_print f a =
@@ -183,12 +178,13 @@ let with_full_print f a =
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
   let old_rawprint = !Flags.raw_print in
   let old_printuniverses = !Constrextern.print_universes in
+  let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in
   Constrextern.print_universes := true;
+  Detyping.print_allow_match_default_clause := false;
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
   Impargs.make_contextual_implicit_args false;
-  Impargs.make_contextual_implicit_args false;
   Dumpglob.pause ();
   try
     let res = f a in
@@ -197,6 +193,7 @@ let with_full_print f a =
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
     Constrextern.print_universes := old_printuniverses;
+    Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
     Dumpglob.continue ();
     res
   with
@@ -206,6 +203,7 @@ let with_full_print f a =
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
 	Flags.raw_print := old_rawprint;
 	Constrextern.print_universes := old_printuniverses;
+        Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
 	Dumpglob.continue ();
 	raise reraise
 
@@ -218,14 +216,14 @@ let with_full_print f a =
 
 type function_info =
     {
-      function_constant : constant;
+      function_constant : Constant.t;
       graph_ind : inductive;
-      equation_lemma : constant option;
-      correctness_lemma : constant option;
-      completeness_lemma : constant option;
-      rect_lemma : constant option;
-      rec_lemma : constant option;
-      prop_lemma : constant option;
+      equation_lemma : Constant.t option;
+      correctness_lemma : Constant.t option;
+      completeness_lemma : Constant.t option;
+      rect_lemma : Constant.t option;
+      rec_lemma : Constant.t option;
+      prop_lemma : Constant.t option;
       is_general : bool; (* Has this function been defined using general recursive definition *)
     }
 
@@ -332,18 +330,18 @@ let discharge_Function (_,finfos) =
 	   is_general = finfos.is_general
 	 }
 
-open Term
-
 let pr_ocst c =
-  Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ())
+  let sigma, env = Pfedit.get_current_context () in
+  Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ())
 
 let pr_info f_info =
+  let sigma, env = Pfedit.get_current_context () in
   str "function_constant := " ++
-  Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+  Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++
   str "function_constant_type := " ++
   (try
-     Printer.pr_lconstr
-       (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
+     Printer.pr_lconstr_env env sigma
+       (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
@@ -351,7 +349,7 @@ let pr_info f_info =
   str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
   str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
   str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
-  str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
+  str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl ()
 
 let pr_table tb =
   let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in
@@ -371,7 +369,7 @@ let in_Function : function_info -> Libobject.obj =
 
 let find_or_none id =
   try Some
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant")
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
     )
   with Not_found -> None
 
@@ -390,7 +388,7 @@ let update_Function finfo =
 			 
 
 let add_Function is_general f =
-  let f_id = Label.to_id (con_label f) in
+  let f_id = Label.to_id (Constant.label f) in
   let equation_lemma = find_or_none (mk_equation_id f_id)
   and correctness_lemma = find_or_none (mk_correct_id f_id)
   and completeness_lemma = find_or_none (mk_complete_id f_id)
@@ -399,7 +397,7 @@ let add_Function is_general f =
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
-    with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive")
+    with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
   in
   let finfos =
     { function_constant = f;
@@ -425,7 +423,6 @@ open Goptions
 
 let functional_induction_rewrite_dependent_proofs_sig = 
   {
-    optsync = false;
     optdepr = false;
     optname = "Functional Induction Rewrite Dependent";
     optkey =  ["Functional";"Induction";"Rewrite";"Dependent"];
@@ -438,7 +435,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t
 
 let function_debug_sig =
   {
-    optsync = false;
     optdepr = false;
     optname = "Function debug";
     optkey =  ["Function_debug"];
@@ -457,7 +453,6 @@ let strict_tcc = ref false
 let is_strict_tcc () = !strict_tcc
 let strict_tcc_sig =
   {
-    optsync = false;
     optdepr = false;
     optname = "Raw Function Tcc";
     optkey =  ["Function_raw_tcc"];
@@ -475,13 +470,17 @@ exception ToShow of exn
 let jmeq () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
-    Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq"
+    EConstr.of_constr @@
+    Universes.constr_of_global @@
+      Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let jmeq_refl () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
-    Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl"
+    EConstr.of_constr @@
+    Universes.constr_of_global @@
+      Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
@@ -489,10 +488,13 @@ let h_intros l =
 
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
-let well_founded = function () -> (coq_constant "well_founded")
-let acc_rel = function () -> (coq_constant "Acc")
-let acc_inv_id = function () -> (coq_constant "Acc_inv")
-let well_founded_ltof = function () ->  (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
+let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded")
+let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
+let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
+
+let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@
+    Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
+
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 
 let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
@@ -501,8 +503,58 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G
     | VarRef id -> EvalVarRef id
     | _ -> assert false;;
 
-let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
+let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
   tclREPEAT
     (List.fold_right
        (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
+
+let decompose_lam_n sigma n =
+  if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive");
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else match EConstr.kind sigma c with
+      | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
+      | Cast (c,_,_)     -> lamdec_rec l n c
+      | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions")
+  in
+  lamdec_rec [] n
+
+let lamn n env b =
+  let open EConstr in
+  let rec lamrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> lamrec (n-1,  l, mkLambda (v,t,b))
+    | _ -> assert false
+  in
+  lamrec (n,env,b)
+
+(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)
+let compose_lam l b = lamn (List.length l) l b
+
+(* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)
+let prodn n env b =
+  let open EConstr in
+  let rec prodrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, mkProd (v,t,b))
+    | _ -> assert false
+  in
+  prodrec (n,env,b)
+
+(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
+let compose_prod l b = prodn (List.length l) l b
+
+type tcc_lemma_value =
+  | Undefined
+  | Value of constr
+  | Not_needed
+
+(* We only "purify" on exceptions. XXX: What is this doing here? *)
+let funind_purify f x =
+  let st = Vernacstate.freeze_interp_state `No in
+  try f x
+  with e ->
+    let e = CErrors.push e in
+    Vernacstate.unfreeze_interp_state st;
+    Exninfo.iraise e