diff options
| author | gregoire | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /tactics/setoid_replace.ml | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
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
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 19 |
1 files changed, 10 insertions, 9 deletions
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 |