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

10 files changed, 118 insertions, 151 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 8276188566..4c2cbf9873 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -33,10 +33,9 @@ type 'a clausenv = {
 type wc = walking_constraints
 
 let new_evar_in_sign env =
-  let hyps = Environ.var_context env in
+  let ids = ids_of_var_context (Environ.var_context env) in
   let ev = new_evar () in
-  DOPN(Evar ev,
-       Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)))
+  DOPN(Evar ev, Array.of_list (List.map (fun id -> VAR id) ids))
 
 let rec whd_evar env sigma = function
   | DOPN(Evar ev,_) as k ->
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b73d19ee91..abfe2305db 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -100,7 +100,7 @@ let w_add_sign (id,t) (wc : walking_constraints) =
   ids_mk (ts_mod
             (fun evr ->
                { focus = evr.focus;
-		 env = push_var (id,t) evr.env;
+		 env = push_var_decl (id,t) evr.env;
 		 decls = evr.decls })
             (ids_it wc))
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fa69b6e73e..6bea1e8199 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -116,11 +116,11 @@ let get_current_proof_name () =
 let add_proof (na,pfs,ts) =
   Edit.create proof_edits (na,pfs,ts,Some !undo_limit)
     
-let del_proof na =
+let delete_proof na =
   try 
     Edit.delete proof_edits na
   with (UserError ("Edit.delete",_)) ->
-    errorlabstrm "Pfedit.del_proof"
+    errorlabstrm "Pfedit.delete_proof"
       [< 'sTR"No such proof" ; msg_proofs false >]
       
 let init_proofs () = Edit.clear proof_edits
@@ -142,7 +142,7 @@ let restart_proof () =
 	errorlabstrm "Pfedit.restart"
           [< 'sTR"No focused proof to restart" ; msg_proofs true >]
     | Some(na,_,ts) -> 
-	del_proof na;
+	delete_proof na;
         start (na,ts);
         set_current_proof na
 
@@ -178,16 +178,15 @@ let undo n =
     errorlabstrm "Pfedit.undo" [< 'sTR"No focused proof"; msg_proofs true >]
 
 (*********************************************************************)
-(*                Proof releasing                                    *)
+(*                  Proof cooking                                    *)
 (*********************************************************************)
 
-let release_proof () =
+let cook_proof () =
   let (pfs,ts) = get_state() 
   and ident = get_current_proof_name () in
   let {evar_concl=concl} = ts.top_goal 
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in
-  del_proof ident;
   (ident,
    ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl },
     strength))
@@ -204,11 +203,9 @@ let check_no_pending_proofs () =
       [< 'sTR"Proof editing in progress" ; (msg_proofs false) ;
          'sTR"Use \"Abort All\" first or complete proof(s)." >]
 
-let abort_proof = del_proof
+let delete_current_proof () = delete_proof (get_current_proof_name ())
 
-let abort_current_proof () = del_proof (get_current_proof_name ())
-
-let abort_all_proofs = init_proofs
+let delete_all_proofs = init_proofs
    
 (*********************************************************************)
 (*              Modifying the current prooftree                      *)
@@ -238,14 +235,6 @@ let solve_nth k tac =
   let pft = get_pftreestate() in
   if not (List.mem (-1) (cursor_of_pftreestate pft)) then 
     mutate (solve_nth_pftreestate k tac)
-    (* ;
-    let pfs =get_pftreestate() in
-    let pf = proof_of_pftreestate pfs in
-    let (pfterm,metamap) = refiner__extract_open_proof pf.goal.hyps pf
-    in (try typing__control_only_guard empty_evd pfterm
-    with e -> (undo 1; raise e));
-    ()) 
-    *)
   else 
     error "cannot apply a tactic when we are descended behind a tactic-node"
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 0bf91510b6..a796cd1f44 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -29,19 +29,19 @@ val refining : unit -> bool
 
 val check_no_pending_proofs : unit -> unit
 
-(*s [abort_proof name] aborts proof of name [name] or failed if no proof
-has this name *)
+(*s [delete_proof name] deletes proof of name [name] or failed if no proof
+    has this name *)
 
-val abort_proof : identifier -> unit
+val delete_proof : identifier -> unit
 
-(* [abort_current_proof ()] aborts current focused proof or failed if
+(* [delete_current_proof ()] deletes current focused proof or failed if
     no proof is focused *)
 
-val abort_current_proof : unit -> unit
+val delete_current_proof : unit -> unit
 
-(* [abort_all_proofs ()] aborts all open proofs if any *)
+(* [delete_all_proofs ()] deletes all open proofs if any *)
 
-val abort_all_proofs : unit -> unit
+val delete_all_proofs : unit -> unit
 
 (*s [undo n] undoes the effect of the last [n] tactics applied to the
     current proof; it fails if no proof is focused or if the ``undo''
@@ -82,13 +82,11 @@ val resume_proof : identifier -> unit
 
 val suspend_proof : unit -> unit
 
-(*s [release_proof ()] turns the current proof into a constant with
-    its name and strength, then remove the proof from the set of
-    pending proofs; it fails if there is no current proof of if it is
-    not completed *)
+(*s [cook_proof ()] turns the current proof (assumed completed)
+    into a constant with its name and strength; it fails if there is
+    no current proof of if it is not completed *)
 
-val release_proof : unit ->
-  identifier * (Declarations.constant_entry * strength)
+val cook_proof : unit -> identifier * (Declarations.constant_entry * strength)
 
 (*s [get_pftreestate ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
@@ -145,22 +143,3 @@ val traverse : int -> unit
 val traverse_nth_goal : int -> unit
 val traverse_next_unproven : unit -> unit
 val traverse_prev_unproven : unit -> unit
-
-(*i N'ont pas à être exportées
-type proof_topstate
-val msg_proofs : bool -> std_ppcmds
-val undo_limit : int ref
-val get_state : unit -> pftreestate * proof_topstate
-val get_topstate : unit -> proof_topstate
-val add_proof : string * pftreestate * proof_topstate -> unit
-val del_proof : string -> unit
-val init_proofs : unit -> unit
-
-val mutate : (pftreestate -> pftreestate) -> unit
-val rev_mutate : (pftreestate -> pftreestate) -> unit
-val start : string * proof_topstate -> unit
-val proof_term : unit -> constr
-val save_anonymous : bool -> string -> unit
-val traverse_to : int list -> unit
-i*)
-
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index e6150fba66..438f0efe3d 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -147,7 +147,7 @@ let ctxt_access sigma sp =
 
 
 let pf_lookup_name_as_renamed hyps ccl s =
-  Detyping.lookup_name_as_renamed (gLOB hyps) ccl s
+  Detyping.lookup_name_as_renamed hyps ccl s
 
 let pf_lookup_index_as_renamed ccl n =
   Detyping.lookup_index_as_renamed ccl n
@@ -166,7 +166,7 @@ open Printer
   term_env *)
 
 let pf_lookup_name_as_renamed hyps ccl s =
-  Detyping.lookup_name_as_renamed (gLOB hyps) ccl s
+  Detyping.lookup_name_as_renamed hyps ccl s
 
 let pf_lookup_index_as_renamed ccl n =
   Detyping.lookup_index_as_renamed ccl n
@@ -174,16 +174,15 @@ let pf_lookup_index_as_renamed ccl n =
 let pr_idl idl = prlist_with_sep pr_spc print_id idl
 
 let pr_goal g =
-  let sign = context g.evar_env in
-  let penv = pr_env_opt sign in
-  let pc = prterm_env_at_top sign g.evar_concl in
+  let penv = pr_context_of g.evar_env in
+  let pc = prterm_env_at_top g.evar_env g.evar_concl in
   [< 'sTR"  "; hV 0 [< penv; 'fNL;
 		       'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
                        'sTR "============================"; 'fNL ;
                        'sTR" " ; pc>]; 'fNL>]
 
 let pr_concl n g =
-  let pc = prterm_env_at_top (context g.evar_env) g.evar_concl in
+  let pc = prterm_env_at_top g.evar_env g.evar_concl in
   [< 'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
      'sTR "subgoal ";'iNT n;'sTR " is:";'cUT;'sTR" " ; pc >]
 
@@ -233,16 +232,9 @@ let pr_seq evd =
     | Some i -> i 
     | None -> anomaly "pr_seq : info = None"
   in
-  let hyps = var_context env in
-  let sign = List.rev (list_of_sign hyps) in
   let pc = pr_ctxt info in
-  let pdcl =
-    prlist_with_sep pr_spc
-      (fun (id,ty) ->
-	 hOV 0 [< print_id id; 'sTR" : ";prterm (body_of_type ty) >])
-      sign 
-  in
-  let pcl = prterm_env_at_top (gLOB hyps) cl in
+  let pdcl = pr_var_context_of env in
+  let pcl = prterm_env_at_top env cl in
   hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
 
 let prgl gl =
@@ -252,13 +244,13 @@ let prgl gl =
 
 let pr_evgl gl =
   let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
-  let phyps = pr_idl (ids_of_sign (var_context gl.evar_env)) in
+  let phyps = pr_idl (ids_of_var_context (var_context gl.evar_env)) in
   let pc = prterm gl.evar_concl in
   hOV 0 [< 'sTR"[[" ; plc; 'sTR"] " ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
 
 let pr_evgl_sign gl = 
   let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
-  let ps = pr_sign (var_context gl.evar_env) in
+  let ps = pr_var_context_of gl.evar_env in
   let pc = prterm gl.evar_concl in
   hOV 0 [< 'sTR"[[" ; plc ; 'sTR"] " ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
 
@@ -352,7 +344,7 @@ let ast_of_cvt_arg = function
   | Integer n       -> num n 
   | Command c       -> ope ("COMMAND",[c])
   | Constr  c       -> 
-      ope ("COMMAND",[ast_of_constr false (assumptions_for_print []) c])
+      ope ("COMMAND",[ast_of_constr false (Global.env ()) c])
   | Clause idl      -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl)
   | Bindings bl     -> ope ("BINDINGS", 
 			    List.map (ast_of_cvt_bind (fun x -> x)) bl)
@@ -360,7 +352,7 @@ let ast_of_cvt_arg = function
       ope ("BINDINGS", 
 	   List.map 
 	     (ast_of_cvt_bind
-		(ast_of_constr false (assumptions_for_print []))) bl)
+		(ast_of_constr false (Global.env ()))) bl)
   | Tacexp ast      -> ope ("TACTIC",[ast])
   | Tac tac -> failwith "TODO: ast_of_cvt_arg: Tac"
   | Redexp red -> failwith "TODO: ast_of_cvt_arg: Redexp"
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 1a16f77448..333287b3ed 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -44,7 +44,7 @@ let norm_goal sigma gl =
   let red_fun = nf_ise1 sigma in
   let ncl = red_fun gl.evar_concl in
   { evar_concl = ncl;
-    evar_env = change_hyps (map_sign_typ (typed_app red_fun)) gl.evar_env;
+    evar_env = map_context red_fun gl.evar_env;
     evar_body = gl.evar_body;
     evar_info = gl.evar_info }
 
@@ -74,9 +74,10 @@ let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
 	let m,l = list_chop h l in 
 	(List.hd fl m) :: (mapshape t (List.tl fl) l)
 
-(* given a proof p, frontier p gives (l,v) where l is the list of goals
+(* frontier : proof_tree -> goal list * validation
+   given a proof p, frontier p gives (l,v) where l is the list of goals
    to be solved to complete the proof, and v is the corresponding validation *)
-
+   
 let rec frontier p =
   match p.ref with
     | None -> 
@@ -230,17 +231,14 @@ let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
 (* rc_of_glsigma : proof sigma -> readable_constraints *)
 let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
 
-(* extract_open_proof : constr signature -> proof
-  -> constr * (int * constr) list
-  takes a constr signature corresponding to global definitions
-  and a (not necessarly complete) proof
-  and gives a pair (pfterm,obl)
+(* extract_open_proof : proof_tree -> constr * (int * constr) list
+  takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
   where pfterm is the constr corresponding to the proof
   and obl is an int*constr list [ (m1,c1) ; ... ; (mn,cn)]
   where the mi are metavariables numbers, and ci are their types.
   Their proof should be completed in order to complete the initial proof *)
 
-let extract_open_proof sign pf =
+let extract_open_proof sigma pf =
   let open_obligations = ref [] in
   let rec proof_extractor vl = function
     | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
@@ -255,42 +253,31 @@ let extract_open_proof sign pf =
     | {ref=Some(Local_constraints lc,[pf])} -> (proof_extractor vl) pf
 	  
     | {ref=None;goal=goal} ->
-	let n_rels = number_of_rels vl in
 	let visible_rels =
           map_succeed
             (fun id ->
-               match lookup_id id vl with
-		 | GLOBNAME _ -> failwith "caught"
-		 | RELNAME(n,_) -> (n,id))
-            (ids_of_sign (evar_hyps goal)) in
-	let sorted_rels = 
-	  Sort.list (fun (n1,_) (n2,_) -> n1>n2) visible_rels in
+               try let n = list_index id vl in (n,id)
+	       with Not_found -> failwith "caught")
+            (ids_of_var_context (evar_hyps goal)) in
+	let sorted_rels =
+	  Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
 	let abs_concl =
           List.fold_right
             (fun (_,id) concl ->
-	       let (_,ty) = lookup_sign id (evar_hyps goal) in
-	       mkNamedProd id (incast_type ty) concl)
+	       let (c,ty) = lookup_id id (evar_hyps goal) in
+	       mkNamedProd_or_LetIn (id,c,ty) concl)
             sorted_rels goal.evar_concl
 	in
+	let ass = Retyping.get_assumption_of goal.evar_env sigma abs_concl in
 	let mv = new_meta() in
-	open_obligations := (mv,abs_concl):: !open_obligations;
+	open_obligations := (mv,ass):: !open_obligations;
 	applist(DOP0(Meta mv),List.map (fun (n,_) -> Rel n) sorted_rels) 
 	  
     | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
   in
-  let pfterm = proof_extractor (gLOB sign) pf in
+  let pfterm = proof_extractor [] pf in
   (pfterm, List.rev !open_obligations)
   
-(* extracts a constr from a proof, and raises an error if the proof is
-   incomplete *)
-
-let extract_proof sign pf =
-  match extract_open_proof sign pf with
-    | t,[] -> t
-    | _ -> errorlabstrm "extract_proof"
-	  [< 'sTR "Attempt to save an incomplete proof" >]
-
-
 (*********************)
 (*   Tacticals       *)
 (*********************)
@@ -554,7 +541,11 @@ let tactic_list_tactic tac gls =
 
 
 
-(* solve_subgoal n tac pf_sigma applies the tactic tac at the nth subgoal of
+(* solve_subgoal :
+     (global_constraints ref * goal list * validation -> 
+         global_constraints ref * goal list * validation) -> 
+      (proof_tree sigma -> proof_tree sigma)
+   solve_subgoal tac pf_sigma applies the tactic tac at the nth subgoal of
    pf_sigma *)
 let solve_subgoal tacl pf_sigma =
   let (sigr,pf) = unpackage pf_sigma in
@@ -587,7 +578,7 @@ type pftreestate = {
 let proof_of_pftreestate pts = pts.tpf
 let is_top_pftreestate pts = pts.tstack = [] 
 let cursor_of_pftreestate pts = List.map fst pts.tstack
-let evc_of_pftreestate pts = pts.tpfsigma
+let evc_of_pftreestate pts = ts_it pts.tpfsigma
 
 let top_goal_of_pftreestate pts = 
   { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
@@ -649,12 +640,12 @@ let change_constraints_pftreestate newgc pts =
 
 (* solve the nth subgoal with tactic tac *)
 let solve_nth_pftreestate n tac pts =
-  let pf = pts.tpf in
-  let rslts =
-    solve_subgoal (theni_tac n tac) {it = pts.tpf;sigma = pts.tpfsigma} in
-  { tpf      = rslts.it;
-    tpfsigma = rslts.sigma;
-    tstack   = pts.tstack }
+ let rslts =
+   solve_subgoal (theni_tac n tac) {it = pts.tpf;sigma = pts.tpfsigma}
+ in
+ { tpf      = rslts.it;
+   tpfsigma = rslts.sigma;
+   tstack   = pts.tstack }
 
 let solve_pftreestate = solve_nth_pftreestate 1
 
@@ -678,15 +669,19 @@ let mk_pftreestate g =
    proof is not complete or the state does not correspond to the head
    of the proof-tree *)
 
+let extract_open_pftreestate pts =
+  extract_open_proof (ts_it pts.tpfsigma) pts.tpf
+
 let extract_pftreestate pts =
   if pts.tstack <> [] then
     errorlabstrm "extract_pftreestate"
       [< 'sTR"Cannot extract from a proof-tree in which we have descended;" ;
          'sPC; 'sTR"Please ascend to the root" >];
-  let env = pts.tpf.goal.evar_env in
-  let hyps = Environ.var_context env in
-  strong whd_betaiotaevar env (ts_it pts.tpfsigma)
-    (extract_proof hyps pts.tpf)
+  let pfterm,subgoals = extract_open_pftreestate pts in
+  if subgoals <> [] then
+   errorlabstrm "extract_proof"
+   [< 'sTR "Attempt to save an incomplete proof" >];
+  strong whd_betaiotaevar pts.tpf.goal.evar_env (ts_it pts.tpfsigma) pfterm
 
 
 (* Focus on the first leaf proof in a proof-tree state *)
@@ -811,18 +806,22 @@ let pr_rule = function
   | Context ctxt -> pr_ctxt ctxt
   | Local_constraints lc -> [< 'sTR"Local constraint change" >]
 
-let thin_sign osign sign =
-  sign_it
-    (fun id ty nsign ->
-       if (not (mem_sign osign id))
-         or (id,ty) <> (lookup_sign id osign)  (* Hum, egalité sur les types *)
-       then add_sign (id,ty) nsign
-       else nsign) sign nil_sign
+exception Different
+
+(* We remove from the var context of env what is already in osign *)
+let thin_sign osign env =
+  process_var_context
+    (fun env (id,c,ty as d) ->
+       try 
+	 if lookup_id id osign = (c,ty) then env
+	 else raise Different
+       with Not_found | Different -> push_var d env)
+    env
 
 let rec print_proof sigma osign pf =
   let {evar_env=env; evar_concl=cl; 
        evar_info=info; evar_body=body} = pf.goal in
-  let env' = change_hyps (fun sign -> thin_sign osign sign) env in
+  let env' = thin_sign osign env in
   match pf.ref with
     | None -> 
 	hOV 0 [< pr_seq {evar_env=env'; evar_concl=cl;
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5c2b24d7fc..8546b0c73c 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -39,10 +39,6 @@ val frontier : transformation_tactic
 val list_pf : proof_tree -> goal list
 val unTAC : tactic -> goal sigma -> proof_tree sigma
 
-val extract_open_proof : 
-  typed_type signature -> proof_tree -> constr * (int * constr) list
-
-
 (*s Tacticals. *)
 
 (* [tclIDTAC] is the identity tactic *)
@@ -114,7 +110,7 @@ type pftreestate
 val proof_of_pftreestate : pftreestate -> proof_tree
 val cursor_of_pftreestate : pftreestate -> int list
 val is_top_pftreestate : pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> global_constraints
+val evc_of_pftreestate : pftreestate -> evar_declarations
 val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 
@@ -127,6 +123,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate
 val weak_undo_pftreestate : pftreestate -> pftreestate
 
 val mk_pftreestate : goal -> pftreestate
+val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
 val extract_pftreestate : pftreestate -> constr
 val first_unproven : pftreestate -> pftreestate
 val last_unproven : pftreestate -> pftreestate
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c95424fb18..cb8eb0c454 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -45,12 +45,6 @@ let constr_of_Constr = function
   | Constr c -> c
   | _ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">]
 
-(* Transforms a type_judgment signature into a (string * constr) list *)
-let make_hyps hyps =
-  let lid = List.map string_of_id (ids_of_sign hyps)
-  and lhyp = List.map body_of_type (vals_of_sign hyps) in
-    List.rev (List.combine lid lhyp)
-
 (* Extracted the constr list from lfun *)
 let rec constr_list goalopt = function
   | (str,VArg(Constr c))::tl -> (id_of_string str,c)::(constr_list goalopt tl)
@@ -62,7 +56,7 @@ let rec constr_list goalopt = function
        (match goalopt with
        | None -> constr_list goalopt tl
        | Some goal ->
-         if List.mem_assoc (string_of_id id) (make_hyps (pf_hyps goal)) then
+         if mem_var_context id (pf_hyps goal) then
            (id_of_string str,VAR id)::(constr_list goalopt tl)
          else
            constr_list goalopt tl))
@@ -287,12 +281,11 @@ let apply_matching pat csr =
      PatternMatchingFailure -> raise No_match
 
 (* Tries to match one hypothesis with a list of hypothesis patterns *)
-let apply_one_hyp_context lmatch mhyps (idhyp,hyp) =
+let apply_one_hyp_context lmatch mhyps (idhyp,bodyopt,hyp) =
   let rec apply_one_hyp_context_rec (idhyp,hyp) mhyps_acc = function
     | (Hyp (idpat,pat))::tl ->
       (try
-         ([idpat,VArg (Identifier
-           (id_of_string idhyp))],verify_metas_coherence lmatch
+         ([idpat,VArg (Identifier idhyp)],verify_metas_coherence lmatch
            (Pattern.matches pat hyp),mhyps_acc@tl)
        with
            PatternMatchingFailure | Not_coherent_metas ->
@@ -307,7 +300,7 @@ let apply_one_hyp_context lmatch mhyps (idhyp,hyp) =
              apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[NoHypId pat])
                tl)
     | [] -> raise No_match in
-  apply_one_hyp_context_rec (idhyp,hyp) [] mhyps
+  apply_one_hyp_context_rec (idhyp,body_of_type hyp) [] mhyps
 
 (* Prepares the lfun list for constr substitutions *)
 let rec make_subs_list = function
@@ -473,7 +466,7 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr =
       (try eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal)) t goal
        with No_match -> apply_match_context evc env lfun lmatch goal tl)
     | (Pat (mhyps,mgoal,mt))::tl ->
-      let hyps = make_hyps (pf_hyps goal)
+      let hyps = pf_hyps goal
       and concl = pf_concl goal in
       (try
          (let lgoal = apply_matching mgoal concl in
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
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 60be331742..6ae4f9ae26 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -34,8 +34,11 @@ val apply_sig_tac :
 val pf_concl              : goal sigma -> constr
 val pf_env                : goal sigma -> env
 val pf_hyps               : goal sigma -> var_context
-val pf_untyped_hyps       : goal sigma -> constr signature
-val pf_nth_hyp            : goal sigma -> int -> identifier * constr
+(*val pf_untyped_hyps       : goal sigma -> (identifier * constr) list*)
+val pf_hyps_types         : goal sigma -> (identifier * constr) list
+val pf_nth_hyp_id         : goal sigma -> int -> identifier
+val pf_last_hyp           : goal sigma -> var_declaration
+val pf_ids_of_hyps        : goal sigma -> identifier list
 val pf_ctxt               : goal sigma -> ctxtty
 val pf_global             : goal sigma -> identifier -> constr
 val pf_parse_const        : goal sigma -> string -> constr
@@ -45,9 +48,9 @@ val pf_execute            : goal sigma -> constr -> unsafe_judgment
 val hnf_type_of           : goal sigma -> constr -> constr
 
 val pf_interp_constr      : goal sigma -> Coqast.t -> constr
-val pf_interp_type : goal sigma -> Coqast.t -> constr
+val pf_interp_type        : goal sigma -> Coqast.t -> constr
 
-val pf_get_hyp             : goal sigma -> identifier -> constr
+val pf_get_hyp_typ        : goal sigma -> identifier -> constr 
 
 val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
 
@@ -88,7 +91,7 @@ type pftreestate
 val proof_of_pftreestate    : pftreestate -> proof_tree
 val cursor_of_pftreestate   : pftreestate -> int list
 val is_top_pftreestate      : pftreestate -> bool
-val evc_of_pftreestate      : pftreestate -> global_constraints
+val evc_of_pftreestate      : pftreestate -> evar_declarations
 val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 val traverse                : int -> pftreestate -> pftreestate
@@ -96,6 +99,7 @@ val weak_undo_pftreestate   : pftreestate -> pftreestate
 val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate       : tactic -> pftreestate -> pftreestate
 val mk_pftreestate          : goal -> pftreestate
+val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
 val extract_pftreestate     : pftreestate -> constr
 val first_unproven          : pftreestate -> pftreestate
 val last_unproven           : pftreestate -> pftreestate