Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 163 insertions, 289 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index cefeb8ae..1f79d73c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml,v 1.80.2.5 2005/12/17 21:15:52 herbelin Exp $ *)
+(* $Id: logic.ml 8696 2006-04-11 07:05:50Z herbelin $ *)
 
 open Pp
 open Util
@@ -25,7 +25,6 @@ open Proof_trees
 open Proof_type
 open Typeops
 open Type_errors
-open Coqast
 open Retyping
 open Evarutil
  
@@ -40,114 +39,72 @@ type refiner_error =
   | 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 _) | 
-    Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ ))) -> true
+let rec catchable_exception = function
+  | Stdpp.Exc_located(_,e) -> catchable_exception e
+  | Util.UserError _ | TypeError _ 
+  | RefinerError _ | Indrec.RecursionSchemeError _
+  | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+  (* unification errors *)
+  | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _|
+      CannotUnifyBindingType _|NotClean _)) -> 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;
-  try let r = tac gl in check := c; r with e -> check := c; raise e
-
 let with_check = Options.with_option check
-   
+
 (************************************************************************)
 (************************************************************************)
 (* 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 (nhyps,cleared_ids) =
+    let fcheck cleared_ids (id,_,_ as d)  =
+      if !check && cleared_ids<>[] then
+	Idset.iter
+	  (fun id' ->
+            if List.mem id' cleared_ids then
+              error (string_of_id id'^
+		        " is used in hypothesis "^string_of_id id))
+	  (global_vars_set_of_decl env d) in
+    clear_hyps ids fcheck gl.evar_hyps in
   let ncl = gl.evar_concl in
-  check_clear_forward rmv (global_vars_set env ncl) "conclusion";
+  if !check && cleared_ids<>[] then
+    Idset.iter
+      (fun id' ->
+        if List.mem id' cleared_ids then
+          error (string_of_id id'^" is used in conclusion"))
+      (global_vars_set env ncl);
   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)] *)
+   returns [tail::(f head (id,_,_) (rev 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"
+  try apply_to_hyp sign id f 
+  with Hyp_not_found -> 
+    if !check then error "No such assumption"
+    else sign
 
 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"
+  try apply_to_hyp_and_dependent_on sign id f g 
+  with Hyp_not_found -> 
+    if !check then error "No such assumption"
+    else sign
 
 let check_typability env sigma c =
   if !check then let _ = type_of env sigma c in () 
@@ -162,26 +119,24 @@ let recheck_typability (what,id) env sigma t =
       ("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')
-
+  let sign =
+    apply_to_hyp_and_dependent_on (named_context_val env) id
+      (fun (_,c,t) _ ->
+	match c with
+	| None -> error ((string_of_id id)^" is not a local definition")
+	| Some c ->(id,None,t))
+      (fun (id',c,t as d) sign ->
+	(if !check then
+	  begin 
+	    let env = reset_with_named_context sign env in
+	    match c with
+	    | None ->  recheck_typability (Some id',id) env sigma t
+	    | Some b ->
+		let b' = mkCast (b,DEFAULTcast, t) in
+		recheck_typability (Some id',id) env sigma b'
+	  end;d))
+  in
+  reset_with_named_context sign env 
 
 (* Auxiliary functions for primitive MOVE tactic
  *
@@ -231,9 +186,16 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
 	  moverec first' middle' right
   in
   if toleft then 
-    List.rev_append (moverec [] [declfrom] left) right
+    let right = 
+      List.fold_right push_named_context_val right empty_named_context_val in
+    List.fold_left (fun sign d -> push_named_context_val d sign)
+      right (moverec [] [declfrom] left) 
   else 
-    List.rev_append left (moverec [] [declfrom] right)
+    let right = 
+      List.fold_right push_named_context_val
+	(moverec [] [declfrom] right) empty_named_context_val in
+    List.fold_left (fun sign d -> push_named_context_val d sign)
+      right left
 
 let check_backward_dependencies sign d =
   if not (Idset.for_all
@@ -255,8 +217,8 @@ let check_forward_dependencies 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]))
+    (fun (_,b,t) _ -> (id2,b,t))
+    (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
 
 let replace_hyp sign id d =
   apply_to_hyp sign id
@@ -264,13 +226,17 @@ let replace_hyp sign id d =
        if !check then
 	 (check_backward_dependencies sign d;
 	  check_forward_dependencies id tail);
-       add_named_decl d sign)
+       d)
 
+(* why we dont check that id does not appear in tail ??? *)
 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))
+  try 
+    insert_after_hyp sign id d 
+      (fun sign ->
+	if !check then check_backward_dependencies sign d)
+  with Hyp_not_found ->
+    if !check then error "No such assumption"
+    else sign
 
 (************************************************************************)
 (************************************************************************)
@@ -282,7 +248,7 @@ 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
+    | Cast(c,_,_) -> collrec acc c
     | (App _| Case _) -> fold_constr collrec acc c
     | _ -> acc
   in 
@@ -311,13 +277,17 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
           raise (RefinerError (OccurMetaGoal conclty));
 	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
 
-    | Cast (t,ty) ->
+    | 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',hdty) =
+	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
+	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
+	  else 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;
@@ -346,12 +316,20 @@ 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 ->
+    | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
 	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
 
+    | Cast (t,_, ty) ->
+	check_typability env sigma ty;
+	mk_refgoals sigma goal goalacc ty t
+
     | App (f,l) ->
-	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
+	let (acc',hdty) = 
+	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
+	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
+	  else mk_hdgoals sigma goal goalacc f
+	in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
 
     | Case (_,p,c,lf) ->
@@ -397,16 +375,13 @@ let error_use_instantiate () =
 
 let convert_hyp sign sigma (id,b,bt as d) =
   apply_to_hyp sign id
-    (fun sign (_,c,ct) _ ->
+    (fun _ (_,c,ct) _ ->
        let env = Global.env_of_context sign in
        if !check && not (is_conv env sigma bt ct) then
-	 (* Just a warning in V8.0bugfix for compatibility *)
-	 msgnl (str "Compatibility warning: Hazardeous change of the type of " ++ pr_id id ++ 
-	       str " (not well-typed in current signature)");
+	 error ("Incorrect change of the type of "^(string_of_id id));
        if !check && not (option_compare (is_conv env sigma) b c) then
-	 msgnl (str "Compatibility warning: Hazardeous change of the body of " ++ pr_id id ++
-	       str " (not well-typed in current signature)");
-       add_named_decl d sign)
+	 error ("Incorrect change of the body of "^(string_of_id id));
+       d)
 
 
 (************************************************************************)
@@ -420,18 +395,18 @@ let prim_refiner r sigma goal =
   match r with
     (* Logical rules *)
     | Intro id ->
-    	if !check && mem_named_context id sign then
+    	if !check && mem_named_context id (named_context_of_val 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)
+	       let sg = mk_goal (push_named_context_val (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)
+		 mk_goal (push_named_context_val (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
@@ -453,11 +428,11 @@ let prim_refiner r sigma goal =
 	       raise (RefinerError IntroNeedsProduct))
 	
     | Cut (b,id,t) ->
-    	if !check && mem_named_context id sign then
+    	if !check && mem_named_context id (named_context_of_val 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
+        let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in
         if b then [sg1;sg2] else [sg2;sg1]  
 
     | FixRule (f,n,rest) ->
@@ -481,9 +456,9 @@ let prim_refiner r sigma goal =
 	      if not (sp=sp') then 
 		error ("fixpoints should be on the same " ^ 
 		       "mutual inductive declaration");
-	      if !check && mem_named_context f sign then 
+	      if !check && mem_named_context f (named_context_of_val sign) then
 		error "name already used in the environment";
-	      mk_sign (add_named_decl (f,None,ar) sign) oth
+	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] -> 
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
 	in 
@@ -506,11 +481,11 @@ let prim_refiner r sigma goal =
         let rec mk_sign sign = function 
           | (f,ar)::oth ->
 	      (try
-                (let _ = Sign.lookup_named f sign in
+                (let _ = lookup_named_val f sign in
                 error "name already used in the environment")
               with
               |	Not_found ->
-                  mk_sign (add_named_decl (f,None,ar) sign) oth)
+                  mk_sign (push_named_context_val (f,None,ar) sign) oth)
 	  | [] -> List.map (fun (_,c) -> mk_goal sign c) all
      	in 
 	mk_sign sign all
@@ -523,7 +498,7 @@ let prim_refiner r sigma goal =
 	sgl
 
     (* Conversion rules *)
-    | Convert_concl cl' ->
+    | 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
@@ -544,18 +519,20 @@ let prim_refiner r sigma goal =
           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 sign' = named_context_val (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 (left,right,declfrom,toleft) = 
+	  split_sign hfrom hto (named_context_of_val 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
+        if !check & id1 <> id2 &&
+	  List.mem id2 (ids_of_named_context (named_context_of_val 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
@@ -566,15 +543,39 @@ let prim_refiner r sigma goal =
 (* Extracting a proof term from the proof tree *)
 
 (* Util *)
+
+type variable_proof_status = ProofVar | SectionVar of identifier
+
+type proof_variable = name * variable_proof_status
+
+let subst_proof_vars = 
+  let rec aux p vars =
+    let _,subst =
+      List.fold_left (fun (n,l) var ->
+        let t = match var with
+          | Anonymous,_ -> l
+          | Name id, ProofVar -> (id,mkRel n)::l
+          | Name id, SectionVar id' -> (id,mkVar id')::l in
+        (n+1,t)) (p,[]) vars
+    in replace_vars (List.rev subst)
+  in aux 1
+         
 let rec rebind id1 id2 = function
-  | [] -> []
-  | id::l -> 
-      if id = id1 then id2::l else
+  | [] -> [Name id2,SectionVar id1]
+  | (na,_ as x)::l -> 
+      if na = Name id1 then (Name id2,ProofVar)::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'
+        if na = Name id2 then (Anonymous,ProofVar)::l' else x::l'
+
+let add_proof_var id vl = (Name id,ProofVar)::vl
+
+let proof_variable_index x = 
+  let rec aux n = function
+    | (Name id,ProofVar)::l when x = id -> n
+    | _::l ->  aux (n+1) l
+    | [] -> raise Not_found
+  in 
+  aux 1
 
 let prim_extractor subfun vl pft =
   let cl = pft.goal.evar_concl in
@@ -582,61 +583,64 @@ let prim_extractor subfun vl pft =
     | 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)
+	       let cty = subst_proof_vars vl ty in
+	       mkLambda (Name id, cty, subfun (add_proof_var 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)
+	       let cb = subst_proof_vars vl b in
+	       let cty = subst_proof_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (add_proof_var 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)
+	       let cty = subst_proof_vars vl ty in
+	       mkLambda (Name id, cty, subfun (add_proof_var 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)
+	       let cb = subst_proof_vars vl b in
+	       let cty = subst_proof_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (add_proof_var 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)
+	mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
+                 subfun (add_proof_var 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 lcty = Array.map (fun (_,_,ar) -> subst_proof_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 newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
+          (add_proof_var 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 lcty = Array.map (fun (_,ar) -> subst_proof_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 newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
+          (add_proof_var 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 
+	let cc = subst_proof_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_concl (t,k)),[pf]) ->
+	if k = DEFAULTcast then subfun vl pf
+	else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
     | 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 *)
+     (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
 	subfun vl pf
 	
     | Some (Prim (ThinBody _),[pf]) ->
@@ -652,133 +656,3 @@ let prim_extractor subfun vl pft =
 
     | 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