1 files changed, 84 insertions, 40 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f56e92414e..7558ac7ac2 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,3 +1,4 @@
+open API
 open Names
 open Pp
 open Libnames
@@ -21,12 +22,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
@@ -49,7 +47,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 +67,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 rt.CAst.v 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 +81,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 rt.CAst.v 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 []
 
@@ -106,12 +104,12 @@ let list_add_set_eq eq_fun x l =
 
 let const_of_id id =
   let _,princ_ref =
-    qualid_of_reference (Libnames.Ident (Loc.ghost,id))
+    qualid_of_reference (Libnames.Ident (Loc.tag 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
@@ -123,15 +121,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  *)
@@ -218,14 +217,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 *)
     }
 
@@ -371,7 +370,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 +389,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 +398,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 +424,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 +436,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 +454,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 +471,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 +489,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 +504,49 @@ 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 Term.constr
+  | Not_needed