diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 17:12:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 17:12:25 +0000 |
| commit | 8db4a882c70008d0eefbbb90b401612906cc9629 (patch) | |
| tree | c0f5e66802510c7eab8c60565e4bb5fba5969194 | |
| parent | 2ff4982f7184aa0cb1ce30f3ad57cd1c0d86c3bb (diff) | |
Changement nommage des hypothèses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@461 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/elim.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index dc89f475e..a9df949ea 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -71,21 +71,23 @@ let rec general_decompose_clause recognizer = (* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste pas si aucune élimination n'est possible *) -let rec general_decompose recognizer c gl = +(* Meilleures stratégies mais perte de compatibilité *) +let up_to_delta = ref false (* true *) +let tmphyp_name = id_of_string "TmpHyp" (* "H" *) + +let general_decompose recognizer c gl = let typc = pf_type_of gl c in (tclTHENS (cut typc) - [(tclTHEN intro + [(tclTHEN (intro_using tmphyp_name) (onLastHyp (general_decompose_clause recognizer))); (exact c)]) gl -let up_to_delta = ref false - let head_in gls indl t = try let ity,_ = if !up_to_delta then find_mrectype (pf_env gls) (project gls) t - else extract_mrectype (pf_env gls) (project gls) t + else extract_mrectype t in List.mem ity indl with Induc -> false |