- déplacement (encore une fois !) des variables existentielles : elles sont

   toujours dans le noyau (en ce sens que Reduction et Typeops les
   connaissent) mais dans un argument supplémentaire A COTE de l'environnement
   (de type unsafe_env)
 - Indtypes et Typing n'utilisent strictement que Evd.empty


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

7 files changed, 311 insertions, 66 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index bf174a59ca..37fce80b7e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -22,8 +22,8 @@ type refiner_error =
 
 exception RefinerError of refiner_error
 
-let conv_leq_goal env arg ty conclty =
-  if not (is_conv_leq env ty conclty) then 
+let conv_leq_goal env sigma arg ty conclty =
+  if not (is_conv_leq env sigma ty conclty) then 
     raise (RefinerError (BadType (arg,ty,conclty)))
 
 let type_of env hyps c =
@@ -32,84 +32,84 @@ let type_of env hyps c =
 let execute_type env ty =
   failwith "TODO: typage type avec VE"
 
-let rec mk_refgoals env goal goalacc conclty trm =
-  let hyps = goal.goal_ev.evar_hyps in
+let rec mk_refgoals env sigma goal goalacc conclty trm =
+  let hyps = goal.evar_hyps in
   match trm with
     | DOP0(Meta mv) ->
 	if occur_meta conclty then
           error "Cannot refine to conclusions with meta-variables";
-	let ctxt = goal.goal_ctxtty in 
-	(mk_goal ctxt hyps (nf_betaiota env conclty))::goalacc, conclty
+	let ctxt = goal.evar_info in 
+	(mk_goal ctxt hyps (nf_betaiota env sigma conclty))::goalacc, conclty
 
     | DOP2(Cast,t,ty) ->
 	let _ = type_of env hyps ty in
-	conv_leq_goal env trm ty conclty;
-	mk_refgoals env goal goalacc ty t
+	conv_leq_goal env sigma trm ty conclty;
+	mk_refgoals env sigma goal goalacc ty t
 
     | DOPN(AppL,cl) ->
-	let (acc',hdty) = mk_hdgoals env goal goalacc (array_hd cl) in
+	let (acc',hdty) = mk_hdgoals env sigma goal goalacc (array_hd cl) in
 	let (acc'',conclty') = 
-	  mk_arggoals env goal acc' hdty (array_list_of_tl cl) in
-	let _ = conv_leq_goal env trm conclty' conclty in
+	  mk_arggoals env sigma goal acc' hdty (array_list_of_tl cl) in
+	let _ = conv_leq_goal env sigma trm conclty' conclty in
         (acc'',conclty')
 
     | DOPN(MutCase _,_) as mc -> 
 	let (_,p,c,lf) = destCase mc in
-	let (acc',lbrty,conclty') = mk_casegoals env goal goalacc p c in
+	let (acc',lbrty,conclty') = mk_casegoals env sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
-            (fun lacc ty fi -> fst (mk_refgoals env goal lacc ty fi))
+            (fun lacc ty fi -> fst (mk_refgoals env sigma goal lacc ty fi))
             acc' lbrty lf 
 	in
-	let _ = conv_leq_goal env trm conclty' conclty in 
+	let _ = conv_leq_goal env sigma trm conclty' conclty in 
 	(acc'',conclty')
 
     | t -> 
 	if occur_meta t then raise (RefinerError (OccurMeta t));
       	let t'ty = type_of env hyps t in
-	conv_leq_goal env t t'ty conclty;
+	conv_leq_goal env sigma t t'ty conclty;
         (goalacc,t'ty)
 
 (* Same as mkREFGOALS but without knowing te type of the term. Therefore,
  * Metas should be casted. *)
 
-and mk_hdgoals env goal goalacc trm =
-  let hyps = goal.goal_ev.evar_hyps in
+and mk_hdgoals env sigma goal goalacc trm =
+  let hyps = goal.evar_hyps in
   match trm with
     | DOP2(Cast,DOP0(Meta mv),ty) ->
 	let _ = type_of env hyps ty in
-	let ctxt = goal.goal_ctxtty in  
-	(mk_goal ctxt hyps (nf_betaiota env ty))::goalacc,ty
+	let ctxt = goal.evar_info in  
+	(mk_goal ctxt hyps (nf_betaiota env sigma ty))::goalacc,ty
 	  
     | DOPN(AppL,cl) ->
-	let (acc',hdty) = mk_hdgoals env goal goalacc (array_hd cl) in
-	mk_arggoals env goal acc' hdty (array_list_of_tl cl)
+	let (acc',hdty) = mk_hdgoals env sigma goal goalacc (array_hd cl) in
+	mk_arggoals env sigma goal acc' hdty (array_list_of_tl cl)
 	
     | DOPN(MutCase _,_) as mc -> 
 	let (_,p,c,lf) = destCase mc in
-	let (acc',lbrty,conclty') = mk_casegoals env goal goalacc p c in
+	let (acc',lbrty,conclty') = mk_casegoals env sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
-            (fun lacc ty fi -> fst (mk_refgoals env goal lacc ty fi))
+            (fun lacc ty fi -> fst (mk_refgoals env sigma goal lacc ty fi))
             acc' lbrty lf 
 	in
 	(acc'',conclty')
 
     | t -> goalacc,type_of env hyps t
 
-and mk_arggoals env goal goalacc funty = function
+and mk_arggoals env sigma goal goalacc funty = function
   | [] -> goalacc,funty
   | harg::tlargs ->
-      (match whd_betadeltaiota env funty with
+      (match whd_betadeltaiota env sigma funty with
 	 | DOP2(Prod,c1,b) ->
-	     let (acc',hargty) = mk_refgoals env goal goalacc c1 harg in
-	     mk_arggoals env goal acc' (sAPP b harg) tlargs
+	     let (acc',hargty) = mk_refgoals env sigma goal goalacc c1 harg in
+	     mk_arggoals env sigma goal acc' (sAPP b harg) tlargs
 	 | t -> raise (RefinerError (CannotApply (t,harg))))
 
-and mk_casegoals env goal goalacc p c= 
-  let (acc',ct) = mk_hdgoals env goal goalacc c in 
-  let (acc'',pt) = mk_hdgoals env goal acc' p in
-  let (_,lbrty,conclty) = type_case_branches env ct pt p c in
+and mk_casegoals env sigma goal goalacc p c= 
+  let (acc',ct) = mk_hdgoals env sigma goal goalacc c in 
+  let (acc'',pt) = mk_hdgoals env sigma goal acc' p in
+  let (_,lbrty,conclty) = type_case_branches env sigma ct pt p c in
   (acc'',lbrty,conclty)
 
 
@@ -209,11 +209,10 @@ let move_after with_dep toleft (left,htfrom,right) hto =
     
 (* Primitive tactics are handled here *)
 
-let prim_refiner r env goal =
-  let ev = goal.goal_ev in
-  let sign = ev.evar_hyps in
-  let cl = ev.evar_concl in
-  let info = goal.goal_ctxtty in
+let prim_refiner r env sigma goal =
+  let sign = goal.evar_hyps in
+  let cl = goal.evar_concl in
+  let info = goal.evar_info in
   match r with
     | { name = Intro; newids = [id] } ->
     	if mem_sign sign id then error "New variable is already declared";
@@ -269,7 +268,7 @@ let prim_refiner r env goal =
             | DOP2(Prod,c1,DLAM(_,b)) -> 
             	if k = 1 then 
 		  (try 
-		     find_minductype env c1 
+		     find_minductype env sigma c1 
 		   with Induc -> 
 		     error "cannot do a fixpoint on a non inductive type")
             	else 
@@ -288,7 +287,7 @@ let prim_refiner r env goal =
             | DOP2(Prod,c1,DLAM(_,b)) -> 
             	if k = 1 then 
 		  (try 
-		     find_minductype env c1 
+		     find_minductype env sigma c1 
 		   with Induc -> 
 		     error "cannot do a fixpoint on a non inductive type")
             	else 
@@ -315,11 +314,11 @@ let prim_refiner r env goal =
 
     | { name = Cofix; hypspecs = []; terms = lar; newids = lf; params = [] } ->
      	let rec check_is_coind cl = 
-          match (whd_betadeltaiota env (whd_castapp cl)) with 
+          match (whd_betadeltaiota env sigma (whd_castapp cl)) with 
             | DOP2(Prod,c1,DLAM(_,b)) -> check_is_coind  b
             | b  -> 
 		(try 
-		   let _ = find_mcoinductype env b in true
+		   let _ = find_mcoinductype env sigma b in true
                  with Induc -> 
 		   error ("All methods must construct elements " ^
 			  "in coinductive types"))
@@ -338,13 +337,13 @@ let prim_refiner r env goal =
 	  
     | { name = Refine; terms = [c] } ->
 	let c = new_meta_variables c in
-	let (sgl,cl') = mk_refgoals env goal [] cl c in
+	let (sgl,cl') = mk_refgoals env sigma goal [] cl c in
 	let sgl = List.rev sgl in
 	sgl
 
     | { name = Convert_concl; terms = [cl'] } ->
     	let cl'ty = type_of env sign cl' in
-	if is_conv_leq env cl' cl then
+	if is_conv_leq env sigma cl' cl then
           let sg = mk_goal info sign (DOP2(Cast,cl',cl'ty)) in
           [sg]
 	else 
@@ -353,7 +352,7 @@ let prim_refiner r env goal =
     | { name = Convert_hyp; hypspecs = [id]; terms = [ty'] } ->
       (* Faut-il garder la sorte d'origine ou celle du converti ?? *)
     	let tj = execute_type env (sign_before id sign) ty' in
-	if is_conv env ty' (snd(lookup_sign id sign)).body then
+	if is_conv env sigma ty' (snd(lookup_sign id sign)).body then
           [mk_goal info (modify_sign id tj sign) cl]
 	else 
 	  error "convert-hyp rule passed non-converting term"
@@ -440,7 +439,6 @@ let extract_constr =
     | DOPN(Abst _,_) as val_0 -> crec vl (abst_value val_0)
     | DOPN(oper,cl) -> DOPN(oper,Array.map (crec vl) cl)
     | DOPL(oper,cl) -> DOPL(oper,List.map (crec vl) cl)
-    | DOP0(Meta _) as c -> c
     | DOP0 _ as c -> c
     | _ -> anomaly "extract_constr : term not matched"
   in 
@@ -448,7 +446,7 @@ let extract_constr =
 
 
 let prim_extractor subfun vl pft =
-  let cl = pft.goal.goal_ev.evar_concl in
+  let cl = pft.goal.evar_concl in
   match pft with
     | { ref = Some (Prim { name = Intro; newids = [id] }, [spf]) } ->
 	(match strip_outer_cast cl with
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 27a50af85b..cc9f108ee8 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -4,11 +4,12 @@
 (*i*)
 open Term
 open Sign
+open Evd
 open Environ
 open Proof_trees
 (*i*)
 
-val prim_refiner : prim_rule -> unsafe_env -> goal -> goal list
+val prim_refiner : prim_rule -> unsafe_env -> 'a evar_map -> goal -> goal list
 
 val prim_extractor : 
   ((typed_type, constr) env -> proof_tree -> constr) -> 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7b3d05eeb4..6c5cadd837 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -3,8 +3,31 @@
 
 (*i*)
 open Pp
+open Sign
+open Declare
+open Proof_trees
 (*i*)
 
 val proof_prompt : unit -> string
 val refining : unit -> bool
 val msg_proofs : bool -> std_ppcmds
+
+val undo_limit : int ref
+val set_undo : int -> unit
+val unset_undo : unit -> unit
+
+type proof_topstate = {
+  top_hyps : context * context;
+  top_goal : goal;
+  top_strength : strength }
+
+val get_state : unit -> pftreestate * proof_topstate
+val get_topstate : unit -> proof_topstate
+val get_pftreestate : unit -> pftreestate
+val get_evmap_sign : int option -> evar_declarations * context
+val set_proof : string option -> unit
+val get_proof : unit -> string
+val list_proofs : unit -> string list
+val add_proof : string * pftreestate * proof_topstate -> unit
+val del_proof : string -> unit
+val init_proofs : unit -> unit
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index a2a10095dc..eb9bc00f83 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -69,9 +69,7 @@ type proof_tree = {
   ref : (rule * proof_tree list) option; 
   subproof : proof_tree option }
 
-and goal = {
-  goal_ev : evar_info;
-  goal_ctxtty : ctxtty }
+and goal = ctxtty evar_info
 
 and rule =
   | Prim of prim_rule
@@ -84,7 +82,7 @@ and ctxtty = {
   mimick : proof_tree option;
   lc     : local_constraints } 
 
-type evar_declarations = goal Intmap.t
+type evar_declarations = ctxtty evar_map
 
 
 let is_bind = function
@@ -96,24 +94,24 @@ let lc_toList lc = Intset.elements lc
 (* Functions on goals *)
 
 let mk_goal ctxt sign cl = 
-  { goal_ev = { evar_hyps = sign; evar_concl = cl; evar_body = Evar_empty };
-    goal_ctxtty = ctxt }
+  { evar_hyps = sign; evar_concl = cl; evar_body = Evar_empty;
+    evar_info = ctxt }
 
 (* Functions on the information associated with existential variables  *)
 
 let mt_ctxt lc = { pgm = None; mimick = None; lc = lc }
 
-let get_ctxt gl = gl.goal_ctxtty
+let get_ctxt gl = gl.evar_info
 
-let get_pgm gl = gl.goal_ctxtty.pgm
+let get_pgm gl = gl.evar_info.pgm
 
 let set_pgm pgm ctxt = { ctxt with pgm = pgm }
 
-let get_mimick gl = gl.goal_ctxtty.mimick
+let get_mimick gl = gl.evar_info.mimick
 
 let set_mimick mimick ctxt = { mimick = mimick; pgm = ctxt.pgm; lc = ctxt.lc }
 
-let get_lc gl = gl.goal_ctxtty.lc
+let get_lc gl = gl.evar_info.lc
 
 (* Functions on proof trees *)
 
@@ -180,7 +178,7 @@ let mt_evcty lc gc =
   ts_mk { focus = lc; sign = nil_sign; decls = gc }
 
 let evc_of_evds evds gl = 
-  ts_mk { focus = (get_lc gl); sign = gl.goal_ev.evar_hyps ; decls = evds }
+  ts_mk { focus = (get_lc gl); sign = gl.evar_hyps ; decls = evds }
 
 let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl
 		       
@@ -188,7 +186,7 @@ let rc_add evc (k,v) =
   ts_mod
     (fun evc -> { focus = (Intset.add k evc.focus);
                   sign  = evc.sign;
-                  decls = Intmap.add k v evc.decls })
+                  decls = Evd.add evc.decls k v })
     evc
 
 let get_hyps  evc = (ts_it evc).sign
@@ -200,7 +198,7 @@ let remap evc (k,v) =
   ts_mod
     (fun evc -> { focus = evc.focus;
                   sign  = evc.sign;
-                  decls = Intmap.add k v evc.decls })
+                  decls = Evd.add evc.decls k v })
     evc
 
 let lc_exists f lc = Intset.fold (fun e b -> (f e) or b) lc false
@@ -209,8 +207,8 @@ let lc_exists f lc = Intset.fold (fun e b -> (f e) or b) lc false
  * on [loc]'s access list, or an evar on [loc]'s access list mentions [sp]. *)
 
 let rec mentions sigma sp loc =
-  let loc_evd = Intmap.find loc (ts_it sigma).decls in 
-  match loc_evd.goal_ev.evar_body with 
+  let loc_evd = Evd.map (ts_it sigma).decls loc in 
+  match loc_evd.evar_body with 
     | Evar_defined _ -> (Intset.mem sp (get_lc loc_evd) 
 			 or lc_exists (mentions sigma sp) (get_lc loc_evd))
     | _ -> false
@@ -220,7 +218,7 @@ let rec mentions sigma sp loc =
  * MENTIONS SIGMA SP LOC' is true. *)
 
 let rec accessible sigma sp loc =
-  let loc_evd = Intmap.find loc (ts_it sigma).decls in 
+  let loc_evd = Evd.map (ts_it sigma).decls loc in 
   lc_exists (fun loc' -> sp = loc' or mentions sigma sp loc') (get_lc loc_evd)
 
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index e6c912b931..69bc496046 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -82,9 +82,7 @@ type proof_tree = {
   ref : (rule * proof_tree list) option; 
   subproof : proof_tree option }
 
-and goal = {
-  goal_ev : evar_info;
-  goal_ctxtty : ctxtty }
+and goal = ctxtty evar_info
 
 and rule =
   | Prim of prim_rule
@@ -97,7 +95,7 @@ and ctxtty = {
   mimick : proof_tree option;
   lc     : local_constraints } 
 
-type evar_declarations = goal Intmap.t
+type evar_declarations = ctxtty evar_map
 
 
 val mk_goal : ctxtty -> typed_type signature -> constr -> goal
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
new file mode 100644
index 0000000000..6125dec8be
--- /dev/null
+++ b/proofs/refiner.ml
@@ -0,0 +1,191 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Stamps
+open Evd
+open Proof_trees
+open Logic
+
+type 'a sigma = { 
+  it : 'a ; 
+  sigma : global_constraints }
+
+type validation = (proof_tree list -> proof_tree)
+type tactic = goal sigma -> (goal list sigma * validation)
+type transformation_tactic = proof_tree -> (goal list * validation)
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+let hypotheses gl = gl.evar_hyps
+let conclusion gl = gl.evar_concl
+
+let sig_it x = x.it
+let sig_sig x = x.sigma
+
+
+let project_with_focus gls = rc_of_gc (gls.sigma) (gls.it)
+
+let pf_status pf = pf.status
+
+let is_complete pf = (Complete_proof = (pf_status pf))
+
+let on_open_proofs f pf = if is_complete pf then pf else f pf
+
+let rec and_status = function
+  | [] -> Complete_proof
+  | Complete_proof :: l -> and_status l
+  | _ -> Incomplete_proof
+
+(* mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]
+   gives
+   [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ;
+   (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ] *)
+
+let rec mapshape nl (fl:(proof_tree list -> proof_tree) list) 
+                    (l : proof_tree list) =
+  match nl with
+    | [] -> []
+    | h::t ->
+	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
+   to be solved to complete the proof, and v is the corresponding validation *)
+
+let rec frontier p =
+  match p.ref with
+    | None -> 
+	([p.goal],
+	 (fun lp' -> 
+	    let p' = List.hd lp' in
+            if p'.goal = p.goal then 
+	      p'
+            else 
+	      errorlabstrm "Refiner.frontier"
+                [< 'sTR"frontier was handed back a ill-formed proof." >]))
+    | Some(r,pfl) ->
+    	let gll,vl = List.split(List.map frontier pfl) in
+    	(List.flatten gll,
+         (fun retpfl ->
+            let pfl' = mapshape (List.map List.length gll) vl retpfl in
+            { status = and_status (List.map pf_status pfl');
+              subproof = p.subproof;
+              goal = p.goal;
+              ref = Some(r,pfl')}))
+
+(* list_pf p is the lists of goals to be solved in order to complete the
+   proof p *)
+
+let list_pf p = fst (frontier p)
+
+let rec nb_unsolved_goals pf = 
+  if is_complete pf then 
+    0 
+  else if is_leaf_proof pf then 
+    1 
+  else 
+    let lpf = children_of_proof pf in 
+    List.fold_left (fun n pf1 -> n + nb_unsolved_goals pf1) 0 lpf
+
+(* leaf g is the canonical incomplete proof of a goal g *)
+
+let leaf g = {
+  status = Incomplete_proof;
+  subproof = None;
+  goal = g;
+  ref = None }
+
+(* Tactics table. *)
+
+let tac_tab = Hashtbl.create 17
+
+let add_tactic s t =
+  if Hashtbl.mem tac_tab s then
+    errorlabstrm ("Refiner.add_tactic: "^s) 
+      [<'sTR "Cannot redeclare a tactic.">];
+  Hashtbl.add tac_tab s t
+
+let overwriting_add_tactic s t =
+  if Hashtbl.mem tac_tab s then begin
+    Hashtbl.remove tac_tab s;
+    warning ("Overwriting definition of tactic "^s)
+  end;
+  Hashtbl.add tac_tab s t
+
+let lookup_tactic s =
+  try 
+    Hashtbl.find tac_tab s
+  with Not_found -> 
+    errorlabstrm "Refiner.lookup_tactic"
+      [< 'sTR"The tactic " ; 'sTR s ; 'sTR" is not installed" >]
+
+
+(* refiner r is a tactic applying the rule r *)
+
+let bad_subproof () =
+  errorlabstrm "Refiner.refiner" [< 'sTR"Bad subproof in validation.">]
+
+let refiner = function
+  | Prim pr ->
+      let prim_fun = prim_refiner pr in
+      (fun goal_sigma ->
+         let sgl = 
+           (try prim_fun (ts_it goal_sigma.sigma) goal_sigma.it
+            with UserError _ as e -> raise e
+              | e -> (mSGNL(Errors.explain_user_exn e);
+                      Errors.reraise_user_exn e))
+	 in 
+	 ({it=sgl; sigma = goal_sigma.sigma},
+          (fun pfl ->
+             if not (for_all2eq (fun g pf -> g = pf.goal) sgl pfl) then
+	       bad_subproof ();
+             { status = and_status (List.map pf_status pfl);
+               goal = goal_sigma.it;
+               subproof = None;
+               ref = Some(r,pfl) })))
+      
+  | Tactic(s,targs) ->
+      let tacfun = lookup_tactic s targs in
+      (fun goal_sigma ->
+         let (sgl_sigma,v) = tacfun goal_sigma in
+         let hidden_proof = v (List.map leaf sgl_sigma.it) in
+         (sgl_sigma,
+          fun spfl ->
+            if not (for_all2eq (fun g pf -> g=pf.goal) sgl_sigma.it spfl) then
+	      bad_subproof ();
+            { status = and_status (List.map pf_status spfl);
+              goal = goal_sigma.it;
+              subproof = Some hidden_proof;
+              ref = Some(r,spfl) }))
+      
+  | ((Context ctxt) as r) ->
+      (fun goal_sigma ->
+         let gl = goal_sigma.it in
+         let sg = mk_goal ctxt gl.hyps gl.concl in
+         ({it=[sg];sigma=goal_sigma.sigma},
+          (fun pfl -> 
+	     let pf = List.hd pfl in
+             if pf.goal <> sg then bad_subproof ();
+             { status = pf.status;
+               goal = gl;
+               subproof = None;
+               ref = Some(r,[pf]) })))
+      
+   (* [Local_constraints lc] makes the local constraints be [lc] *)
+
+  | ((Local_constraints lc) as r) ->
+      (fun goal_sigma ->
+         let gl = goal_sigma.it  in
+         let ctxt = outSOME gl.info in 
+         let sg = mkGOAL ctxt gl.hyps gl.concl in
+	 ({it=[sg];sigma=goal_sigma.sigma},
+          (fun pfl -> 
+	     let pf = List.hd pfl in
+             if pf.goal <> sg then bad_subproof ();
+             { status = pf.status;
+               goal = gl;
+               subproof = None;
+               ref = Some(r,[pf]) })))
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
new file mode 100644
index 0000000000..3e0b202c26
--- /dev/null
+++ b/proofs/refiner.mli
@@ -0,0 +1,36 @@
+
+(* $Id$ *)
+
+(*i*)
+open Proof_trees
+(*i*)
+
+type 'a sigma = { 
+  it : 'a ; 
+  sigma : global_constraints }
+
+val sig_it  : 'a sigma -> 'a
+val sig_sig : 'a sigma -> global_constraints
+
+val project_with_focus : goal sigma -> readable_constraints
+
+val unpackage : 'a sigma -> global_constraints ref * 'a
+val repackage : global_constraints ref -> 'a -> 'a sigma
+val apply_sig_tac :
+  global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
+
+type validation = (proof_tree list -> proof_tree)
+
+type tactic = goal sigma -> (goal list sigma * validation)
+
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+val add_tactic             : string -> (tactic_arg list -> tactic) -> unit
+val overwriting_add_tactic : string -> (tactic_arg list -> tactic) -> unit
+val lookup_tactic          : string -> (tactic_arg list) -> tactic
+
+val hide_tactic : 
+  string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
+
+val overwrite_hidden_tactic : 
+  string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)