Leminv API using EConstr.

3 files changed, 37 insertions, 23 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 37c82ff646..5c296b343f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -450,7 +450,6 @@ let raw_inversion inv_kind id status names =
         CErrors.user_err  msg
     in
     let IndType (indf,realargs) = find_rectype env sigma t in
-    let realargs = List.map EConstr.of_constr realargs in
     let evdref = ref sigma in
     let (elim_predicate, args) =
       make_inv_predicate env evdref indf realargs id status concl in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a942384184..62e78b5886 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -11,8 +11,9 @@ open CErrors
 open Util
 open Names
 open Term
-open Vars
 open Termops
+open EConstr
+open Vars
 open Namegen
 open Evd
 open Printer
@@ -31,9 +32,17 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
+let nlocal_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  NamedDecl.LocalAssum (na, inj t)
+
+let nlocal_def (na, b, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  NamedDecl.LocalDef (na, inj b, inj t)
+
 let no_inductive_inconstr env sigma constr =
   (str "Cannot recognize an inductive predicate in " ++
-     pr_lconstr_env env sigma constr ++
+     pr_lconstr_env env sigma (EConstr.Unsafe.to_constr constr) ++
      str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
      spc () ++ str "or of the type of constructors" ++ spc () ++
      str "is hidden by constant definitions.")
@@ -116,15 +125,15 @@ let max_prefix_sign lid sign =
     | id::l -> snd (max_rec (id, sign_prefix id sign) l)
 *)
 let rec add_prods_sign env sigma t =
-  match kind_of_term (whd_all env sigma (EConstr.of_constr t)) with
+  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
     | Prod (na,c1,b) ->
-	let id = id_of_name_using_hdchar env t na in
+	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b'
+        add_prods_sign (push_named (nlocal_assum (id,c1)) env) sigma b'
     | LetIn (na,c1,t1,b) ->
-	let id = id_of_name_using_hdchar env t na in
+	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b'
+        add_prods_sign (push_named (nlocal_def (id,c1,t1)) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates whether the inversion lemma is dependent or not.
@@ -147,6 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
   let pty,goal =
     if dep_option  then
       let pty = make_arity env true indf sort in
+      let pty = EConstr.of_constr pty in
       let goal =
 	mkProd
 	  (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
@@ -154,7 +164,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       pty,goal
     else
       let i = mkAppliedInd ind in
-      let ivars = global_vars env sigma (EConstr.of_constr i) in
+      let ivars = global_vars env sigma i in
       let revargs,ownsign =
 	fold_named_context
 	  (fun env d (revargs,hyps) ->
@@ -169,7 +179,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
       (pty,goal)
   in
-  let npty = nf_all env sigma (EConstr.of_constr pty) in
+  let npty = nf_all env sigma pty in
   let extenv = push_named (LocalAssum (p,npty)) env in
   extenv, goal
 
@@ -183,7 +193,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
 let inversion_scheme env sigma t sort dep_option inv_op =
   let (env,i) = add_prods_sign env sigma t in
   let ind =
-    try find_rectype env sigma (EConstr.of_constr i)
+    try find_rectype env sigma i
     with Not_found ->
       user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
   in
@@ -192,18 +202,20 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   in
   assert
     (List.subset
-       (global_vars env sigma (EConstr.of_constr invGoal))
+       (global_vars env sigma invGoal)
        (ids_of_named_context (named_context invEnv)));
   (*
     user_err ~hdr:"lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
+  let invGoal = EConstr.Unsafe.to_constr invGoal in
   let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       tclTHEN intro (onLastHypId inv_op)) pf)
   in
   let pfterm = List.hd (Proof.partial_proof pf) in
+  let pfterm = EConstr.of_constr pfterm in
   let global_named_context = Global.named_context_val () in
   let ownSign = ref begin
     fold_named_context
@@ -216,18 +228,19 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let { sigma=sigma } = Proof.V82.subgoals pf in
   let sigma = Evd.nf_constraints sigma in
   let rec fill_holes c =
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Evar (e,args) ->
 	let h = next_ident_away (Id.of_string "H") !avoid in
 	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
 	avoid := h::!avoid;
-	ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign;
+	ownSign := Context.Named.add (nlocal_assum (h,ty)) !ownSign;
 	applist (mkVar h, inst)
-    | _ -> Constr.map fill_holes c
+    | _ -> EConstr.map sigma fill_holes c
   in
   let c = fill_holes pfterm in
   (* warning: side-effect on ownSign *)
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
+  let invProof = EConstr.Unsafe.to_constr invProof in
   let p = Evarutil.nf_evars_universes sigma invProof in
     p, Evd.universe_context sigma
 
@@ -245,6 +258,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
   let env = Global.env () in
   let evd = ref (Evd.from_env env) in
   let c = Constrintern.interp_type_evars env evd com in
+  let c = EConstr.of_constr c in
   let sigma, sort = Pretyping.interp_sort !evd comsort in
   try
     add_inversion_lemma na env sigma c sort bool tac
@@ -258,14 +272,16 @@ let add_inversion_lemma_exn na com comsort bool tac =
 
 let lemInv id c gls =
   try
-    let clause = mk_clenv_type_of gls (EConstr.of_constr c) in
+    let clause = mk_clenv_type_of gls c in
     let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
     Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
   with
     | NoSuchBinding ->
+        let c = EConstr.Unsafe.to_constr c in
 	user_err 
 	  (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
+        let c = EConstr.Unsafe.to_constr c in
 	 user_err ~hdr:"LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
 	      pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
@@ -291,5 +307,5 @@ let lemInvIn id c ids =
 let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
 
 let lemInv_clause id c = function
-  | [] -> lemInv_gen id (EConstr.Unsafe.to_constr c)
-  | l -> lemInvIn_gen id (EConstr.Unsafe.to_constr c) l
+  | [] -> lemInv_gen id c
+  | l -> lemInvIn_gen id c l
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bae1ad48cf..59ffd8b626 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2896,8 +2896,7 @@ let old_generalize_dep ?(with_let=false) c gl =
 	  -> id::tothin
       | _ -> tothin
   in
-  let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in
-  let cl' = EConstr.of_constr cl' in
+  let cl' = it_mkNamedProd_or_LetIn (EConstr.of_constr (Tacmach.pf_concl gl)) to_quantify in
   let body =
     if with_let then
       match EConstr.kind sigma c with
@@ -4256,11 +4255,11 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
     let env = Proofview.Goal.env gl in
     let sigma = Sigma.to_evar_map sigma in
     let concl = Tacmach.New.pf_nf_concl gl in
+    let concl = EConstr.of_constr concl in
     let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in
-    let dep_in_concl = Option.cata (fun id -> occur_var env sigma id (EConstr.of_constr concl)) false hyp0 in
+    let dep_in_concl = Option.cata (fun id -> occur_var env sigma id concl) false hyp0 in
     let dep = dep_in_hyps || dep_in_concl in
     let tmpcl = it_mkNamedProd_or_LetIn concl deps in
-    let tmpcl = EConstr.of_constr tmpcl in
     let s = Retyping.get_sort_family_of env sigma tmpcl in
     let deps_cstr =
       List.fold_left
@@ -5008,7 +5007,7 @@ let abstract_subproof id gk tac =
 	else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, empty_named_context_val) in
   let id = next_global_ident_away id (pf_ids_of_hyps gl) in
-  let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
+  let concl = it_mkNamedProd_or_LetIn (EConstr.of_constr (Proofview.Goal.concl gl)) sign in
   let concl =
     try flush_and_check_evars !evdref concl
     with Uninstantiated_evar _ ->