From bf578ad5e2f63b7a36aeaef5e0597101db1bd24a Mon Sep 17 00:00:00 2001
From: gregoire
Date: Fri, 2 Dec 2005 10:01:15 +0000
Subject: 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
---
 tactics/setoid_replace.ml | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'tactics/setoid_replace.ml')

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 5cd163364b..316f3c2766 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1464,7 +1464,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
               | (he::tl) as a->
                  let typnf = Reduction.whd_betadeltaiota env typ in
                   match kind_of_term typnf with
-                    Cast (typ,_) ->
+                    Cast (typ,_,_) ->
                      find_non_dependent_function env c c_args_rev typ
                       f_args_rev a_rev a
                   | Prod (name,s,t) ->
@@ -1676,7 +1676,7 @@ let syntactic_but_representation_of_marked_but hole_relation hole_direction =
        else
         let c_is_proper =
          let typ = mkApp (rel_out, [| c ; c |]) in
-          mkCast (Evarutil.mk_new_meta (),typ)
+          mkCast (Evarutil.mk_new_meta (),DEFAULTcast, typ)
         in
          mkApp ((Lazy.force coq_ProperElementToKeep),
           [| hole_relation ; hole_direction; precise_out ;
@@ -1759,7 +1759,8 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
      let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
       let th' = mkApp (proj, [|impl2; impl1; th|]) in
        Tactics.refine
-        (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl in
+        (mkApp (th',[|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|]))
+	gl in
    let if_output_relation_is_if gl =
     let th =
      apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
@@ -1767,15 +1768,15 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
     in
      let new_but = Termops.replace_term c1 c2 but in
       Tactics.refine
-       (mkApp (th, [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl
-   in
-    if output_relation = (Lazy.force coq_iff_relation) then
+       (mkApp (th, [|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|]))
+       gl in
+   if output_relation = (Lazy.force coq_iff_relation) then
      if_output_relation_is_iff gl
-    else
+   else
      if_output_relation_is_if gl
   with
-   Optimize ->
-    !general_rewrite (input_direction = Left2Right) (snd hyp) gl
+    Optimize ->
+      !general_rewrite (input_direction = Left2Right) (snd hyp) gl
 
 let analyse_hypothesis gl c =
  let ctype = pf_type_of gl c in
-- 
cgit v1.2.3