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 /contrib/rtauto | |
| 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 'contrib/rtauto')
| -rw-r--r-- | contrib/rtauto/Rtauto.v | 4 | ||||
| -rw-r--r-- | contrib/rtauto/refl_tauto.ml | 5 |
2 files changed, 5 insertions, 4 deletions
diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v index d1cb802755..342c03dbac 100644 --- a/contrib/rtauto/Rtauto.v +++ b/contrib/rtauto/Rtauto.v @@ -18,7 +18,7 @@ Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t. Ltac clean:=try (simpl;congruence). Inductive form:Set:= -Atom : positive -> form + Atom : positive -> form | Arrow : form -> form -> form | Bot | Conjunct : form -> form -> form @@ -395,4 +395,4 @@ exact (Reflect (empty \ A \ B \ C) (I_Or_r (I_And (Ax 2) (Ax 4))))))). Qed. Print toto. -*)
\ No newline at end of file +*) diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml index 0865a825c9..801122476e 100644 --- a/contrib/rtauto/refl_tauto.ml +++ b/contrib/rtauto/refl_tauto.ml @@ -113,7 +113,7 @@ let rec make_form atom_env gls term = Arrow (fa,fb) else make_atom atom_env (normalize term) - | Cast(a,b) -> + | Cast(a,_,_) -> make_form atom_env gls a | Ind ind -> if ind = Lazy.force li_False then @@ -273,7 +273,8 @@ let rtauto_tac gls= (pf_env gls) (Tacmach.project gls) gl <> InProp then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in - let hyps=make_hyps gamma gls [gl] gls.it.evar_hyps in + let hyps=make_hyps gamma gls [gl] + (Environ.named_context_of_val gls.it.evar_hyps) in let formula= List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in let search_fun = |