Passage à des contextes de vars et de rels pouvant contenir des déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 6 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 9471b5d258..1488b06dee 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -40,19 +40,27 @@ let pf_env gls = (sig_it gls).evar_env
 let pf_hyps gls = var_context (sig_it gls).evar_env
 
 let pf_concl gls = (sig_it gls).evar_concl
-
+(*
 let pf_untyped_hyps gls  =
   let sign = Environ.var_context (pf_env gls) in
   map_sign_typ (fun x -> body_of_type x) sign
+*)
+let pf_hyps_types gls  =
+  let sign = Environ.var_context (pf_env gls) in
+  List.map (fun (id,_,x) -> (id,body_of_type x)) sign
+
+let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
 
-let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
+let pf_last_hyp gl = List.hd (pf_hyps gl)
 
-let pf_get_hyp gls id = 
+let pf_get_hyp_typ gls id = 
   try 
-    snd (lookup_sign id (pf_untyped_hyps gls))
+    body_of_type (snd (lookup_id id (pf_hyps gls)))
   with Not_found -> 
     error ("No such hypothesis : " ^ (string_of_id id))
 
+let pf_ids_of_hyps gls = ids_of_var_context (var_context (pf_env gls))
+
 let pf_ctxt gls      = get_ctxt (sig_it gls)
 
 let pf_interp_constr gls c =
@@ -135,6 +143,7 @@ let solve_pftreestate       = solve_pftreestate
 let weak_undo_pftreestate   = weak_undo_pftreestate
 let mk_pftreestate          = mk_pftreestate
 let extract_pftreestate     = extract_pftreestate
+let extract_open_pftreestate = extract_open_pftreestate
 let first_unproven          = first_unproven
 let last_unproven           = last_unproven
 let nth_unproven            = nth_unproven
@@ -218,6 +227,12 @@ let unTAC            = unTAC
 
 let refiner = refiner
 
+(* This does not check that the variable name is not here *)
+let unsafe_introduction id =
+  without_check
+    (refiner (Prim { name = Intro; newids = [id];
+                     hypspecs = []; terms = []; params = [] }))
+
 let introduction id pf =
   refiner (Prim { name = Intro; newids = [id];
                   hypspecs = []; terms = []; params = [] }) pf
@@ -259,7 +274,7 @@ let mutual_cofix lf lar pf =
     
 let rename_bound_var_goal gls =
   let { evar_env = env; evar_concl = cl } as gl = sig_it gls in 
-  let ids = ids_of_sign (Environ.var_context env) in
+  let ids = ids_of_var_context (Environ.var_context env) in
   convert_concl (rename_bound_var ids cl) gls
     
 
@@ -473,7 +488,7 @@ open Printer
 
 let pr_com sigma goal com =
   prterm (rename_bound_var 
-            (ids_of_sign (var_context goal.evar_env)) 
+            (ids_of_var_context (var_context goal.evar_env)) 
             (Astterm.interp_constr sigma goal.evar_env com))
 
 let pr_one_binding sigma goal = function