Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 786 insertions, 0 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
new file mode 100644
index 00000000..3cc44a0f
--- /dev/null
+++ b/proofs/logic.ml
@@ -0,0 +1,786 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: logic.ml,v 1.80.2.1 2004/07/16 19:30:49 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Evd
+open Term
+open Termops
+open Sign
+open Environ
+open Reductionops
+open Inductive
+open Inductiveops
+open Typing
+open Proof_trees
+open Proof_type
+open Typeops
+open Type_errors
+open Coqast
+open Retyping
+open Evarutil
+ 
+type refiner_error =
+
+  (* Errors raised by the refiner *)
+  | BadType of constr * constr * constr
+  | OccurMeta of constr
+  | OccurMetaGoal of constr
+  | CannotApply of constr * constr
+  | NotWellTyped of constr
+  | NonLinearProof of constr
+
+  (* Errors raised by the tactics *)
+  | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
+  | CannotGeneralize of constr
+  | IntroNeedsProduct
+  | DoesNotOccurIn of constr * identifier
+  | NoOccurrenceFound of constr
+
+exception RefinerError of refiner_error
+
+open Pretype_errors
+
+let catchable_exception = function
+  | Util.UserError _ | TypeError _ | RefinerError _
+  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
+    Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true
+  | _ -> false
+
+let error_cannot_unify (m,n) =
+  raise (RefinerError (CannotUnify (m,n)))
+
+(* Tells if the refiner should check that the submitted rules do not
+   produce invalid subgoals *)
+let check = ref false
+
+let without_check tac gl =
+  let c = !check in
+  check := false;
+  let r = tac gl in
+  check := c;
+  r
+
+let with_check tac gl =
+  let c = !check in
+  check := true;
+  let r = tac gl in
+  check := c;
+  r
+   
+(************************************************************************)
+(************************************************************************)
+(* Implementation of the structural rules (moving and deleting
+   hypotheses around) *)
+
+let check_clear_forward cleared_ids used_ids whatfor =
+  if !check && cleared_ids<>[] then
+    Idset.iter
+      (fun id' ->
+        if List.mem id' cleared_ids then
+          error (string_of_id id'^" is used in "^whatfor))
+      used_ids
+
+(* The Clear tactic: it scans the context for hypotheses to be removed
+   (instead of iterating on the list of identifier to be removed, which
+   forces the user to give them in order). *)
+let clear_hyps ids gl =
+  let env = Global.env() in
+  let (nhyps,rmv) =
+    Sign.fold_named_context
+      (fun (id,c,ty as d) (hyps,rmv) ->
+        if List.mem id ids then
+          (hyps,id::rmv)
+        else begin
+          check_clear_forward rmv (global_vars_set_of_decl env d)
+            ("hypothesis "^string_of_id id);
+          (add_named_decl d hyps, rmv)
+        end)
+      gl.evar_hyps
+      ~init:(empty_named_context,[]) in
+  let ncl = gl.evar_concl in
+  check_clear_forward rmv (global_vars_set env ncl) "conclusion";
+  mk_goal nhyps ncl
+
+(* The ClearBody tactic *)
+
+(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
+   returns [tail::(f head (id,_,_) tail)] *)
+let apply_to_hyp sign id f =
+  let found = ref false in
+  let sign' =
+    fold_named_context_both_sides
+      (fun head (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f head d tail
+	 end else 
+	   add_named_decl d head)
+      sign ~init:empty_named_context
+  in
+  if (not !check) || !found then sign' else error "No such assumption"
+
+(* Same but with whole environment *)
+let apply_to_hyp2 env id f =
+  let found = ref false in
+  let env' =
+    fold_named_context_both_sides
+      (fun env (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f env d tail
+	 end else 
+	   push_named d env)
+      (named_context env) ~init:(reset_context env)
+  in
+  if (not !check) || !found then env' else error "No such assumption"
+
+let apply_to_hyp_and_dependent_on sign id f g =
+  let found = ref false in
+  let sign =
+    Sign.fold_named_context
+      (fun (idc,_,_ as d) oldest ->
+         if idc = id then (found := true; add_named_decl (f d) oldest)
+         else if !found then add_named_decl (g d) oldest
+         else add_named_decl d oldest)
+      sign ~init:empty_named_context
+  in
+  if (not !check) || !found then sign else error "No such assumption"
+
+let check_typability env sigma c =
+  if !check then let _ = type_of env sigma c in () 
+
+let recheck_typability (what,id) env sigma t =
+  try check_typability env sigma t
+  with _ ->
+    let s = match what with
+      | None -> "the conclusion"
+      | Some id -> "hypothesis "^(string_of_id id) in
+    error
+      ("The correctness of "^s^" relies on the body of "^(string_of_id id))
+  
+let remove_hyp_body env sigma id =
+  apply_to_hyp2 env id
+    (fun env (_,c,t) tail ->
+       match c with
+         | None -> error ((string_of_id id)^" is not a local definition")
+         | Some c ->
+             let env' = push_named (id,None,t) env in
+             if !check then 
+               ignore
+                 (Sign.fold_named_context 
+                    (fun (id',c,t as d) env'' ->
+                       (match c with
+                          | None -> 
+                              recheck_typability (Some id',id) env'' sigma t
+                          | Some b ->
+                              let b' = mkCast (b,t) in
+                              recheck_typability (Some id',id) env'' sigma b');
+                       push_named d env'')
+                    (List.rev tail) ~init:env');
+             env')
+
+
+(* Auxiliary functions for primitive MOVE tactic
+ *
+ * [move_after with_dep toleft (left,(hfrom,typfrom),right) hto] moves
+ * hyp [hfrom] just after the hyp [hto] which belongs to the hyps on the 
+ * left side [left] of the full signature if [toleft=true] or to the hyps 
+ * on the right side [right] if [toleft=false].
+ * If [with_dep] then dependent hypotheses are moved accordingly. *)
+
+let split_sign hfrom hto l =
+  let rec splitrec left toleft = function
+    | [] -> error ("No such hypothesis : " ^ (string_of_id hfrom))
+    | (hyp,c,typ) as d :: right ->
+      	if hyp = hfrom then 
+	  (left,right,d,toleft) 
+      	else 
+	  splitrec (d::left) (toleft or (hyp = hto)) right
+  in 
+  splitrec [] false l
+
+let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
+  let env = Global.env() in
+  let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
+    if toleft
+    then occur_var_in_decl env hyp2 d
+    else occur_var_in_decl env hyp d2
+  in
+  let rec moverec first middle = function
+    | [] -> error ("No such hypothesis : " ^ (string_of_id hto))
+    | (hyp,_,_) as d :: right ->
+	let (first',middle') =
+      	  if List.exists (test_dep d) middle then 
+	    if with_dep & (hyp <> hto) then 
+	      (first, d::middle)
+            else 
+	      error 
+		("Cannot move "^(string_of_id idfrom)^" after "
+		 ^(string_of_id hto)
+		 ^(if toleft then ": it occurs in " else ": it depends on ")
+		 ^(string_of_id hyp))
+          else 
+	    (d::first, middle)
+	in
+      	if hyp = hto then 
+	  (List.rev first')@(List.rev middle')@right
+      	else 
+	  moverec first' middle' right
+  in
+  if toleft then 
+    List.rev_append (moverec [] [declfrom] left) right
+  else 
+    List.rev_append left (moverec [] [declfrom] right)
+
+let check_backward_dependencies sign d =
+  if not (Idset.for_all
+	    (fun id -> mem_named_context id sign)
+	    (global_vars_set_of_decl (Global.env()) d))
+  then
+    error "Can't introduce at that location: free variable conflict"
+
+
+let check_forward_dependencies id tail =
+  let env = Global.env() in
+  List.iter
+    (function (id',_,_ as decl) ->
+       if occur_var_in_decl env id decl then
+	 error ((string_of_id id) ^ " is used in hypothesis " 
+		^ (string_of_id id')))
+    tail
+
+
+let rename_hyp id1 id2 sign =
+  apply_to_hyp_and_dependent_on sign id1
+    (fun (_,b,t) -> (id2,b,t))
+    (map_named_declaration (replace_vars [id1,mkVar id2]))
+
+let replace_hyp sign id d =
+  apply_to_hyp sign id
+    (fun sign _ tail ->
+       if !check then
+	 (check_backward_dependencies sign d;
+	  check_forward_dependencies id tail);
+       add_named_decl d sign)
+
+let insert_after_hyp sign id d =
+  apply_to_hyp sign id
+    (fun sign d' _ ->
+       if !check then check_backward_dependencies sign d;
+       add_named_decl d (add_named_decl d' sign))
+
+(************************************************************************)
+(************************************************************************)
+(* Implementation of the logical rules *)
+
+(* Will only be used on terms given to the Refine rule which have meta 
+variables only in Application and Case *)
+
+let collect_meta_variables c = 
+  let rec collrec acc c = match kind_of_term c with
+    | Meta mv -> mv::acc
+    | Cast(c,_) -> collrec acc c
+    | (App _| Case _) -> fold_constr collrec acc c
+    | _ -> acc
+  in 
+  List.rev(collrec [] c)
+
+let check_conv_leq_goal env sigma arg ty conclty =
+  if !check & not (is_conv_leq env sigma ty conclty) then 
+    raise (RefinerError (BadType (arg,ty,conclty)))
+
+let goal_type_of env sigma c =
+  (if !check then type_of else Retyping.get_type_of) env sigma c
+
+let rec mk_refgoals sigma goal goalacc conclty trm =
+  let env = evar_env goal in
+  let hyps = goal.evar_hyps in
+(*
+   if  not (occur_meta trm) then
+    let t'ty = (unsafe_machine env sigma trm).uj_type in 	
+    let _ = conv_leq_goal env sigma trm t'ty conclty in
+      (goalacc,t'ty)
+  else
+*)
+  match kind_of_term trm with
+    | Meta _ ->
+	if occur_meta conclty then
+          raise (RefinerError (OccurMetaGoal conclty));
+	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
+
+    | Cast (t,ty) ->
+	check_typability env sigma ty;
+	check_conv_leq_goal env sigma trm ty conclty;
+	mk_refgoals sigma goal goalacc ty t
+
+    | App (f,l) ->
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	let (acc'',conclty') =
+	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
+	check_conv_leq_goal env sigma trm conclty' conclty;
+        (acc'',conclty')
+
+    | Case (_,p,c,lf) ->
+	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
+	check_conv_leq_goal env sigma trm conclty' conclty;
+	let acc'' = 
+	  array_fold_left2
+            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
+            acc' lbrty lf 
+	in
+	(acc'',conclty')
+
+    | _ -> 
+	if occur_meta trm then raise (RefinerError (OccurMeta trm));
+      	let t'ty = goal_type_of env sigma trm in
+	check_conv_leq_goal env sigma trm 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 sigma goal goalacc trm =
+  let env = evar_env goal in
+  let hyps = goal.evar_hyps in
+  match kind_of_term trm with
+    | Cast (c,ty) when isMeta c ->
+	check_typability env sigma ty;
+	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
+
+    | App (f,l) ->
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	mk_arggoals sigma goal acc' hdty (Array.to_list l)
+
+    | Case (_,p,c,lf) ->
+	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
+	let acc'' = 
+	  array_fold_left2
+            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
+            acc' lbrty lf 
+	in
+	(acc'',conclty')
+
+    | _ -> goalacc, goal_type_of env sigma trm
+
+and mk_arggoals sigma goal goalacc funty = function
+  | [] -> goalacc,funty
+  | harg::tlargs as allargs ->
+      let t = whd_betadeltaiota (evar_env goal) sigma funty in
+      match kind_of_term t with
+	| Prod (_,c1,b) ->
+	    let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
+	    mk_arggoals sigma goal acc' (subst1 harg b) tlargs
+	| LetIn (_,c1,_,b) ->
+	    mk_arggoals sigma goal goalacc (subst1 c1 b) allargs
+	| _ -> raise (RefinerError (CannotApply (t,harg)))
+
+and mk_casegoals sigma goal goalacc p c =
+  let env = evar_env goal in
+  let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
+  let (acc'',pt) = mk_hdgoals sigma goal acc' p in
+  let pj = {uj_val=p; uj_type=pt} in 
+  let indspec =
+    try find_mrectype env sigma ct
+    with Not_found -> anomaly "mk_casegoals" in
+  let (lbrty,conclty) =
+    type_case_branches_with_names env indspec pj c in
+  (acc'',lbrty,conclty)
+
+
+let error_use_instantiate () =
+  errorlabstrm "Logic.prim_refiner"
+    (str"cannot intro when there are open metavars in the domain type" ++
+       spc () ++ str"- use Instantiate")
+
+let convert_hyp sign sigma (id,b,bt as d) =
+  apply_to_hyp sign id
+    (fun sign (_,c,ct) _ ->
+       let env = Global.env_of_context sign in
+       if !check && not (is_conv env sigma bt ct) &&
+         not (option_compare (is_conv env sigma) b c) then
+	   error "convert-hyp rule passed non-converting term";
+       add_named_decl d sign)
+
+
+(************************************************************************)
+(************************************************************************)
+(* Primitive tactics are handled here *)
+
+let prim_refiner r sigma goal =
+  let env = evar_env goal in
+  let sign = goal.evar_hyps in
+  let cl = goal.evar_concl in
+  match r with
+    (* Logical rules *)
+    | Intro id ->
+    	if !check && mem_named_context id sign then
+	  error "New variable is already declared";
+        (match kind_of_term (strip_outer_cast cl) with
+	   | Prod (_,c1,b) ->
+	       if occur_meta c1 then error_use_instantiate();
+	       let sg = mk_goal (add_named_decl (id,None,c1) sign)
+			  (subst1 (mkVar id) b) in
+	       [sg]
+	   | LetIn (_,c1,t1,b) ->
+	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
+	       let sg =
+		 mk_goal (add_named_decl (id,Some c1,t1) sign)
+		   (subst1 (mkVar id) b) in
+	       [sg]
+	   | _ ->
+	       raise (RefinerError IntroNeedsProduct))
+	
+    | Intro_replacing id ->
+	(match kind_of_term (strip_outer_cast cl) with
+           | Prod (_,c1,b) ->
+	       if occur_meta c1 then error_use_instantiate();
+	       let sign' = replace_hyp sign id (id,None,c1) in
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
+	       [sg]
+           | LetIn (_,c1,t1,b) ->
+	       if occur_meta c1 then error_use_instantiate();
+	       let sign' = replace_hyp sign id (id,Some c1,t1) in
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
+	       [sg]
+	   | _ ->
+	       raise (RefinerError IntroNeedsProduct))
+	
+    | Cut (b,id,t) ->
+    	if !check && mem_named_context id sign then
+	  error "New variable is already declared";
+        if occur_meta t then error_use_instantiate();
+        let sg1 = mk_goal sign (nf_betaiota t) in
+        let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in
+        if b then [sg1;sg2] else [sg2;sg1]  
+
+    | FixRule (f,n,rest) ->
+     	let rec check_ind env k cl = 
+          match kind_of_term (strip_outer_cast cl) with 
+            | Prod (na,c1,b) -> 
+            	if k = 1 then 
+		  try 
+		    fst (find_inductive env sigma c1)
+		  with Not_found -> 
+		    error "cannot do a fixpoint on a non inductive type"
+            	else 
+		  check_ind (push_rel (na,None,c1) env) (k-1) b
+            | _ -> error "not enough products"
+	in
+	let (sp,_) = check_ind env n cl in
+	let all = (f,n,cl)::rest in
+     	let rec mk_sign sign = function 
+	  | (f,n,ar)::oth ->
+	      let (sp',_)  = check_ind env n ar in 
+	      if not (sp=sp') then 
+		error ("fixpoints should be on the same " ^ 
+		       "mutual inductive declaration");
+	      if !check && mem_named_context f sign then 
+		error "name already used in the environment";
+	      mk_sign (add_named_decl (f,None,ar) sign) oth
+	  | [] -> 
+	      List.map (fun (_,_,c) -> mk_goal sign c) all
+	in 
+	mk_sign sign all
+	
+    | Cofix (f,others) ->
+     	let rec check_is_coind env cl = 
+	  let b = whd_betadeltaiota env sigma cl in
+          match kind_of_term b with
+            | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
+            | _ -> 
+		try 
+		  let _ = find_coinductive env sigma b in ()
+                with Not_found -> 
+		  error ("All methods must construct elements " ^
+			  "in coinductive types")
+	in
+	let all = (f,cl)::others in
+     	List.iter (fun (_,c) -> check_is_coind env c) all;
+        let rec mk_sign sign = function 
+          | (f,ar)::oth ->
+	      (try
+                (let _ = Sign.lookup_named f sign in
+                error "name already used in the environment")
+              with
+              |	Not_found ->
+                  mk_sign (add_named_decl (f,None,ar) sign) oth)
+	  | [] -> List.map (fun (_,c) -> mk_goal sign c) all
+     	in 
+	mk_sign sign all
+
+    | Refine c ->
+        if not (list_distinct (collect_meta_variables c)) then
+          raise (RefinerError (NonLinearProof c));
+	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
+	let sgl = List.rev sgl in
+	sgl
+
+    (* Conversion rules *)
+    | Convert_concl cl' ->
+	check_typability env sigma cl';
+	if (not !check) || is_conv_leq env sigma cl' cl then
+          let sg = mk_goal sign cl' in
+          [sg]
+	else 
+	  error "convert-concl rule passed non-converting term"
+
+    | Convert_hyp (id,copt,ty) ->
+	[mk_goal (convert_hyp sign sigma (id,copt,ty)) cl]
+
+    (* And now the structural rules *)
+    | Thin ids -> 
+	[clear_hyps ids goal]
+
+    | ThinBody ids ->
+	let clear_aux env id =
+          let env' = remove_hyp_body env sigma id in
+          if !check then recheck_typability (None,id) env' sigma cl;
+          env'
+	in
+	let sign' = named_context (List.fold_left clear_aux env ids) in
+     	let sg = mk_goal sign' cl in
+     	[sg]
+
+    | Move (withdep, hfrom, hto) ->
+  	let (left,right,declfrom,toleft) = split_sign hfrom hto sign in
+  	let hyps' = 
+	  move_after withdep toleft (left,declfrom,right) hto in
+  	[mk_goal hyps' cl]
+
+    | Rename (id1,id2) ->
+        if !check & id1 <> id2 & List.mem id2 (ids_of_named_context sign) then
+          error ((string_of_id id2)^" is already used");
+        let sign' = rename_hyp id1 id2 sign in
+        let cl' = replace_vars [id1,mkVar id2] cl in
+        [mk_goal sign' cl']
+
+(************************************************************************)
+(************************************************************************)
+(* Extracting a proof term from the proof tree *)
+
+(* Util *)
+let rec rebind id1 id2 = function
+  | [] -> []
+  | id::l -> 
+      if id = id1 then id2::l else
+        let l' = rebind id1 id2 l in
+        if id = id2 then
+          (* TODO: find a more elegant way to hide a variable *)
+          (id_of_string "_@")::l'
+        else id::l'
+
+let prim_extractor subfun vl pft =
+  let cl = pft.goal.evar_concl in
+  match pft.ref with
+    | Some (Prim (Intro id), [spf]) ->
+	(match kind_of_term (strip_outer_cast cl) with
+	   | Prod (_,ty,_) ->
+	       let cty = subst_vars vl ty in
+	       mkLambda (Name id, cty, subfun (id::vl) spf)
+	   | LetIn (_,b,ty,_) ->
+	       let cb = subst_vars vl b in
+	       let cty = subst_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
+	   | _ -> error "incomplete proof!")
+	
+    | Some (Prim (Intro_replacing id),[spf]) ->
+	(match kind_of_term (strip_outer_cast cl) with
+	   | Prod (_,ty,_) ->
+	       let cty = subst_vars vl ty in
+	       mkLambda (Name id, cty, subfun (id::vl) spf)
+	   | LetIn (_,b,ty,_) ->
+	       let cb = subst_vars vl b in
+	       let cty = subst_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
+	   | _ -> error "incomplete proof!")
+
+    | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
+        let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
+	mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2)
+
+    | Some (Prim (FixRule (f,n,others)),spfl) ->
+	let all = Array.of_list ((f,n,cl)::others) in
+	let lcty = Array.map (fun (_,_,ar) -> subst_vars vl ar) all in
+	let names = Array.map (fun (f,_,_) -> Name f) all in
+	let vn = Array.map (fun (_,n,_) -> n-1) all in
+	let newvl = List.fold_left (fun vl (id,_,_)->(id::vl)) (f::vl)others in
+	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
+	mkFix ((vn,0),(names,lcty,lfix))	
+
+    | Some (Prim (Cofix (f,others)),spfl) ->
+	let all = Array.of_list ((f,cl)::others) in
+	let lcty = Array.map (fun (_,ar) -> subst_vars vl ar) all in
+	let names  = Array.map (fun (f,_) -> Name f) all in
+	let newvl = List.fold_left (fun vl (id,_)->(id::vl)) (f::vl) others in 
+	let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
+	mkCoFix (0,(names,lcty,lfix))
+	  
+    | Some (Prim (Refine c),spfl) ->
+	let mvl = collect_meta_variables c in
+	let metamap = List.combine mvl (List.map (subfun vl) spfl) in
+	let cc = subst_vars vl c in 
+	plain_instance metamap cc
+
+    (* Structural and conversion rules do not produce any proof *)
+    | Some (Prim (Convert_concl _),[pf]) ->
+	subfun vl pf
+	
+    | Some (Prim (Convert_hyp _),[pf]) ->
+	subfun vl pf
+
+    | Some (Prim (Thin _),[pf]) ->
+     (* No need to make ids Anonymous in vl: subst_vars take the more recent *)
+	subfun vl pf
+	
+    | Some (Prim (ThinBody _),[pf]) ->
+	subfun vl pf
+	
+    | Some (Prim (Move _),[pf]) ->
+	subfun vl pf
+
+    | Some (Prim (Rename (id1,id2)),[pf]) ->
+	subfun (rebind id1 id2 vl) pf
+
+    | Some _ -> anomaly "prim_extractor"
+
+    | None-> error "prim_extractor handed incomplete proof"
+	  
+(* Pretty-printer *)
+
+open Printer
+
+let prterm x = prterm_env (Global.env()) x
+
+let pr_prim_rule_v7 = function
+  | Intro id -> 
+      str"Intro " ++ pr_id id
+	
+  | Intro_replacing id -> 
+      (str"intro replacing "  ++ pr_id id)
+	
+  | Cut (b,id,t) ->
+      if b then
+        (str"Assert " ++ prterm t)
+      else
+        (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]")
+	
+  | FixRule (f,n,[]) ->
+      (str"Fix " ++ pr_id f ++ str"/" ++ int n)
+      
+  | FixRule (f,n,others) -> 
+      let rec print_mut = function
+	| (f,n,ar)::oth -> 
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth
+        | [] -> mt () in
+      (str"Fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut others)
+
+  | Cofix (f,[]) ->
+      (str"Cofix " ++ pr_id f)
+
+  | Cofix (f,others) ->
+      let rec print_mut = function
+	| (f,ar)::oth ->
+	  (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth)
+        | [] -> mt () in
+      (str"Cofix " ++ pr_id f ++  str" with " ++ print_mut others)
+
+  | Refine c -> 
+      str(if occur_meta c then "Refine " else "Exact ") ++
+      Constrextern.with_meta_as_hole prterm c
+      
+  | Convert_concl c ->
+      (str"Change "  ++ prterm c)
+      
+  | Convert_hyp (id,None,t) ->
+      (str"Change "  ++ prterm t  ++ spc ()  ++ str"in "  ++ pr_id id)
+
+  | Convert_hyp (id,Some c,t) ->
+      (str"Change "  ++ prterm c  ++ spc ()  ++ str"in "
+       ++ pr_id id ++ str" (Type of "  ++ pr_id id ++ str ")")
+      
+  | Thin ids ->
+      (str"Clear "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | ThinBody ids ->
+      (str"ClearBody "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | Move (withdep,id1,id2) ->
+      (str (if withdep then "Dependent " else "") ++
+	 str"Move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+  | Rename (id1,id2) ->
+      (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+
+let pr_prim_rule_v8 = function
+  | Intro id -> 
+      str"intro " ++ pr_id id
+	
+  | Intro_replacing id -> 
+      (str"intro replacing "  ++ pr_id id)
+	
+  | Cut (b,id,t) ->
+      if b then
+        (str"assert " ++ prterm t)
+      else
+        (str"cut " ++ prterm t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
+	
+  | FixRule (f,n,[]) ->
+      (str"fix " ++ pr_id f ++ str"/" ++ int n)
+      
+  | FixRule (f,n,others) -> 
+      let rec print_mut = function
+	| (f,n,ar)::oth -> 
+           pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth
+        | [] -> mt () in
+      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
+         str" with " ++ print_mut others)
+
+  | Cofix (f,[]) ->
+      (str"cofix " ++ pr_id f)
+
+  | Cofix (f,others) ->
+      let rec print_mut = function
+	| (f,ar)::oth ->
+	  (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth)
+        | [] -> mt () in
+      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
+
+  | Refine c -> 
+      str(if occur_meta c then "refine " else "exact ") ++
+      Constrextern.with_meta_as_hole prterm c
+      
+  | Convert_concl c ->
+      (str"change "  ++ prterm c)
+      
+  | Convert_hyp (id,None,t) ->
+      (str"change "  ++ prterm t  ++ spc ()  ++ str"in "  ++ pr_id id)
+
+  | Convert_hyp (id,Some c,t) ->
+      (str"change "  ++ prterm c  ++ spc ()  ++ str"in "
+       ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
+      
+  | Thin ids ->
+      (str"clear "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | ThinBody ids ->
+      (str"clearbody "  ++ prlist_with_sep pr_spc pr_id ids)
+      
+  | Move (withdep,id1,id2) ->
+      (str (if withdep then "dependent " else "") ++
+	 str"move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+  | Rename (id1,id2) ->
+      (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+
+let pr_prim_rule t =
+  if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t