Changement des named_context

Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs


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

11 files changed, 140 insertions, 154 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index e653345da..6a0ea6096 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -42,7 +42,7 @@ let clenv_cast_meta clenv =
   let rec crec u =
     match kind_of_term u with
       | App _ | Case _ -> crec_hd u
-      | Cast (c,_) when isMeta c -> u
+      | Cast (c,_,_) when isMeta c -> u
       | _  -> map_constr crec u
 	    
   and crec_hd u =
@@ -51,7 +51,7 @@ let clenv_cast_meta clenv =
 	  (try 
             let b = Typing.meta_type clenv.env mv in
 	    if occur_meta b then u
-            else mkCast (mkMeta mv, b)
+            else mkCast (mkMeta mv, DEFAULTcast, b)
 	  with Not_found -> u)
       | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
       | Case(ci,p,c,br) ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0c9fe0119..26848802e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -69,77 +69,45 @@ 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 () 
@@ -154,26 +122,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
  *
@@ -223,9 +189,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
@@ -247,8 +220,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
@@ -256,13 +229,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
 
 (************************************************************************)
 (************************************************************************)
@@ -274,7 +251,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 
@@ -303,7 +280,7 @@ 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
@@ -338,11 +315,11 @@ 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) ->
+    | Cast (t,_, ty) ->
 	check_typability env sigma ty;
 	mk_refgoals sigma goal goalacc ty t
 
@@ -393,13 +370,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
 	 error ("Incorrect change of the type of "^(string_of_id id));
        if !check && not (option_compare (is_conv env sigma) b c) then
 	 error ("Incorrect change of the body of "^(string_of_id id));
-       add_named_decl d sign)
+       d)
 
 
 (************************************************************************)
@@ -413,18 +390,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]
 	   | _ ->
@@ -446,11 +423,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) ->
@@ -474,9 +451,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 
@@ -499,11 +476,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
@@ -516,7 +493,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
@@ -537,18 +514,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
@@ -622,9 +601,9 @@ let prim_extractor subfun vl pft =
 	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,cl)
     | Some (Prim (Convert_hyp _),[pf]) ->
 	subfun vl pf
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index eca13c56c..8871e7e00 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -76,7 +76,7 @@ val get_undo : unit -> int option
     declare the built constructions as a coercion or a setoid morphism) *)
 
 val start_proof : 
-  identifier -> goal_kind -> named_context -> constr
+  identifier -> goal_kind -> named_context_val -> constr
     -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 73a6bd9a8..1b691e258 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -21,7 +21,7 @@ open Proof_type
 (* This module declares readable constraints, and a few utilities on
    constraints and proof trees *)
 
-val mk_goal : named_context -> constr -> goal
+val mk_goal : named_context_val -> constr -> goal
 
 val rule_of_proof     : proof_tree -> rule
 val ref_of_proof      : proof_tree -> (rule * proof_tree list)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index c20b01636..db3c0e7e2 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -32,7 +32,7 @@ type prim_rule =
   | FixRule of identifier * int * (identifier * int * constr) list
   | Cofix of identifier * (identifier * constr) list
   | Refine of constr
-  | Convert_concl of types
+  | Convert_concl of types * cast_kind
   | Convert_hyp of named_declaration
   | Thin of identifier list
   | ThinBody of identifier list
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index cecda38c5..e22273058 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -32,7 +32,7 @@ type prim_rule =
   | FixRule of identifier * int * (identifier * int * constr) list
   | Cofix of identifier * (identifier * constr) list
   | Refine of constr
-  | Convert_concl of types
+  | Convert_concl of types * cast_kind 
   | Convert_hyp of named_declaration
   | Thin of identifier list
   | ThinBody of identifier list
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 8e02a7b27..2fed1cd2c 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -20,6 +20,13 @@ open Tacred
 open Closure
 open RedFlags
 
+
+(* call by value normalisation function using the virtual machine *)
+let cbv_vm env _ c =
+  let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
+  Vconv.cbv_vm env c ctyp
+
+
 let set_opaque_const sp = 
   Conv_oracle.set_opaque_const sp;
   Csymtable.set_opaque_const sp
@@ -45,10 +52,6 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-(* call by value reduction functions using virtual machine *)
-let cbv_vm env _ c =
-  let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
-  Vconv.cbv_vm env c ctyp
 
 (* Generic reduction: reduction functions used in reduction tactics *)
 
@@ -91,16 +94,19 @@ let declare_red_expr s f =
     red_expr_tab := Stringmap.add s f !red_expr_tab
 
 let reduction_of_red_expr = function
-  | Red internal -> if internal then try_red_product else red_product
-  | Hnf -> hnf_constr
-  | Simpl (Some (_,c as lp)) -> contextually (is_reference c) lp nf
-  | Simpl None -> nf
-  | Cbv f -> cbv_norm_flags (make_flag f)
-  | Lazy f -> clos_norm_flags (make_flag f)
-  | Unfold ubinds -> unfoldn ubinds
-  | Fold cl -> fold_commands cl
-  | Pattern lp -> pattern_occs lp
+  | Red internal -> 
+      if internal then (try_red_product,DEFAULTcast) 
+      else (red_product,DEFAULTcast)
+  | Hnf -> (hnf_constr,DEFAULTcast)
+  | Simpl (Some (_,c as lp)) -> 
+      (contextually (is_reference c) lp nf,DEFAULTcast)
+  | Simpl None -> (nf,DEFAULTcast)
+  | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
+  | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
+  | Unfold ubinds -> (unfoldn ubinds,DEFAULTcast)
+  | Fold cl -> (fold_commands cl,DEFAULTcast)
+  | Pattern lp -> (pattern_occs lp,DEFAULTcast)
   | ExtraRedExpr s ->
-      (try Stringmap.find s !red_expr_tab
+      (try (Stringmap.find s !red_expr_tab,DEFAULTcast)
       with Not_found -> error("unknown user-defined reduction \""^s^"\""))
-  | CbvVm -> cbv_vm 
+  | CbvVm -> (cbv_vm ,VMcast)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 7146f7f5e..1c9393d7f 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -14,12 +14,11 @@ open Closure
 open Rawterm
 open Reductionops
 
-(* Call by value strategy (uses virtual machine) *)
-val cbv_vm : reduction_function
 
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
-val reduction_of_red_expr : red_expr -> reduction_function
+val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
+(* [true] if we should use the vm to verify the reduction *)
 
 val declare_red_expr : string -> reduction_function -> unit
 
@@ -29,3 +28,8 @@ val set_transparent_const : constant -> unit
 
 val set_opaque_var      : identifier -> unit
 val set_transparent_var : identifier -> unit
+
+
+
+(* call by value normalisation function using the virtual machine *)
+val cbv_vm : reduction_function
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index fecddbefb..fa29f5b4d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -41,7 +41,7 @@ let and_status = List.fold_left (+) 0
 (* Getting env *)
 
 let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
-let pf_hyps gls = (sig_it gls).evar_hyps
+let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps
 
 (* Normalizing evars in a goal. Called by tactic Local_constraints
    (i.e. when the sigma of the proof tree changes). Detect if the
@@ -51,11 +51,7 @@ let norm_goal sigma gl =
   let ncl = red_fun gl.evar_concl in
   let ngl =
     { evar_concl = ncl;
-      evar_hyps =
-      Sign.fold_named_context 
-        (fun (d,b,ty) sign ->
-          add_named_decl (d, option_app red_fun b, red_fun ty) sign)
-        gl.evar_hyps ~init:empty_named_context;
+      evar_hyps = map_named_val red_fun gl.evar_hyps; 
       evar_body = gl.evar_body} in
   if ngl = gl then None else Some ngl
 
@@ -288,11 +284,11 @@ let extract_open_proof sigma pf =
             (fun id ->
                try let n = list_index id vl in (n,id)
 	       with Not_found -> failwith "caught")
-            (ids_of_named_context goal.evar_hyps) in
+            (ids_of_named_context (named_context_of_val goal.evar_hyps)) in
 	let sorted_rels =
 	  Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
         let sorted_env =
-          List.map (fun (n,id) -> (n,Sign.lookup_named id goal.evar_hyps))
+          List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps))
             sorted_rels in
 	let abs_concl =
           List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c)
@@ -776,7 +772,8 @@ let extract_pftreestate pts =
       else
         str "Attempt to save a proof with existential variables still non-instantiated");
   let env = Global.env_of_context pts.tpf.goal.evar_hyps in
-  strong whd_betaiotaevar env pts.tpfsigma pfterm
+  strong whd_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm
+  (* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
   (***
   local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
   ***)
@@ -900,7 +897,7 @@ let tclINFO (tac : tactic) gls =
   let (sgl,v) as res = tac gls in 
   begin try 
     let pf = v (List.map leaf (sig_it sgl)) in
-    let sign = (sig_it gls).evar_hyps in
+    let sign = named_context_of_val (sig_it gls).evar_hyps in
     msgnl (hov 0 (str" == " ++
                   !pp_info (project gls) sign pf))
   with e when catchable_exception e -> 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 816fdf932..7ac7b185b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -92,7 +92,7 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
 let pf_reduction_of_red_expr gls re c = 
-  reduction_of_red_expr re (pf_env gls) (project gls) c 
+  (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c 
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_reduce = pf_apply
@@ -115,7 +115,8 @@ let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls)
 
-let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, c2)))
+let pf_check_type gls c1 c2 = 
+  ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
 
 (************************************)
 (* Tactics handling a list of goals *)
@@ -190,8 +191,8 @@ let internal_cut_rev_no_check id t gl =
 let refine_no_check c gl = 
   refiner (Prim (Refine c)) gl
 
-let convert_concl_no_check c gl = 
-  refiner (Prim (Convert_concl c)) gl
+let convert_concl_no_check c sty gl = 
+  refiner (Prim (Convert_concl (c,sty))) gl
 
 let convert_hyp_no_check d gl =
   refiner (Prim (Convert_hyp d)) gl
@@ -218,8 +219,10 @@ let mutual_cofix f others gl =
     
 let rename_bound_var_goal gls =
   let { evar_hyps = sign; evar_concl = cl } = sig_it gls in 
-  let ids = ids_of_named_context sign in
-  convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls
+  let ids = ids_of_named_context (named_context_of_val sign) in
+  convert_concl_no_check 
+    (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls 
+
 
 
 (* Versions with consistency checks *)
@@ -229,7 +232,7 @@ let intro_replacing id = with_check (intro_replacing_no_check id)
 let internal_cut d t     = with_check (internal_cut_no_check d t)
 let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t)
 let refine c           = with_check (refine_no_check c)
-let convert_concl d    = with_check (convert_concl_no_check d)
+let convert_concl d sty = with_check (convert_concl_no_check d sty)
 let convert_hyp d      = with_check (convert_hyp_no_check d)
 let thin l             = with_check (thin_no_check l)
 let thin_body c        = with_check (thin_body_no_check c)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 66cb97fac..817f934db 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -127,7 +127,7 @@ val intro_replacing_no_check  : identifier -> tactic
 val internal_cut_no_check     : identifier -> types -> tactic
 val internal_cut_rev_no_check : identifier -> types -> tactic
 val refine_no_check           : constr -> tactic
-val convert_concl_no_check    : types -> tactic
+val convert_concl_no_check    : types -> cast_kind -> tactic
 val convert_hyp_no_check      : named_declaration -> tactic
 val thin_no_check             : identifier list -> tactic
 val thin_body_no_check        : identifier list -> tactic
@@ -145,10 +145,7 @@ val intro_replacing  : identifier -> tactic
 val internal_cut     : identifier -> types -> tactic
 val internal_cut_rev : identifier -> types -> tactic
 val refine           : constr -> tactic
-val convert_concl    : constr -> tactic
-val convert_hyp      : named_declaration -> tactic
-val thin             : identifier list -> tactic
-val convert_concl    : types -> tactic
+val convert_concl    : types -> cast_kind -> tactic
 val convert_hyp      : named_declaration -> tactic
 val thin             : identifier list -> tactic
 val thin_body        : identifier list -> tactic