From 1dccf4412cf9f5903c6291e08f2001c895babfd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 25 Mar 2014 19:27:44 +0100
Subject: Moving some tactic code to the new engine.

---
 proofs/clenv.ml    |  4 ++--
 proofs/clenv.mli   |  4 ++--
 proofs/tacmach.ml  | 13 ++++++++++++-
 proofs/tacmach.mli | 10 +++++++---
 4 files changed, 23 insertions(+), 8 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 966d247e0..444043dbe 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -496,8 +496,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
 let make_clenv_binding_env_apply env sigma n =
   make_clenv_binding_gen true n env sigma
 	
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma
-let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma
+let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma
+let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 7731c4ca2..9a985a842 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -100,10 +100,10 @@ val make_clenv_binding_env_apply :
    clausenv
 
 val make_clenv_binding_apply :
-  Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
+  env -> evar_map -> int option -> constr * constr -> constr bindings ->
    clausenv
 val make_clenv_binding :
-  Goal.goal sigma -> constr * constr -> constr bindings -> clausenv
+  env -> evar_map -> constr * constr -> constr bindings -> clausenv
 
 (** if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a9146a96a..943974489 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -221,6 +221,7 @@ module New = struct
   let pf_type_of gl t =
     pf_apply type_of gl t
 
+  let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
 
   let pf_ids_of_hyps gl =
     (** We only get the identifiers in [hyps] *)
@@ -253,11 +254,21 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     List.hd hyps
 
-  let pf_nf_concl gl =
+  let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) =
     (** We normalize the conclusion just after *)
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Proofview.Goal.sigma gl in
     nf_evar sigma concl
 
+  let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+
+  let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
+
+  let pf_reduce_to_quantified_ind gl t =
+    pf_apply reduce_to_quantified_ind gl t
+
+  let pf_hnf_type_of gl t =
+    pf_whd_betadeltaiota gl (pf_get_type_of gl t)
+
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 9a53560b6..bf0ce04a1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -134,15 +134,19 @@ module New : sig
   val pf_global : identifier -> 'a Proofview.Goal.t -> constr
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
 
-  val pf_type_of : 'b Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_get_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
   val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : 'b Proofview.Goal.t -> identifier list
-  val pf_hyps_types : 'b Proofview.Goal.t -> (identifier * types) list
+  val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+  val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
 
   val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration
   val pf_get_hyp_typ        : identifier -> [ `NF ] Proofview.Goal.t -> types
   val pf_last_hyp           : [ `NF ] Proofview.Goal.t -> named_declaration
 
   val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> inductive * types
+  val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
 end
-- 
cgit v1.2.3