diff options
| author | filliatr | 2000-03-30 18:26:15 +0000 |
|---|---|---|
| committer | filliatr | 2000-03-30 18:26:15 +0000 |
| commit | e65106b4799afd27eb1aecf6d2d42b098fe7ec89 (patch) | |
| tree | df705534c7a128463de07a79522895075e6a946f /tactics | |
| parent | a345bf314e82b7cf33eb31034b04310b98bd915b (diff) | |
erreurs lexicales dans les patterns (manquait des espaces)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@359 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/pattern.ml | 2 | ||||
| -rw-r--r-- | tactics/tauto.ml | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/tactics/pattern.ml b/tactics/pattern.ml index 78fa139741..23b6da6e46 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -321,7 +321,7 @@ let match_with_equation t = let is_equation t = op2bool (match_with_equation t) let match_with_nottype t = - let notpat = put_pat mmk "(?1->?2)" in + let notpat = put_pat mmk "(?1 -> ?2)" in try (match dest_somatch t notpat with | [arg;mind] when is_empty_type mind -> Some (mind,arg) diff --git a/tactics/tauto.ml b/tactics/tauto.ml index 76efe0958e..4fcfc0264e 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -52,8 +52,8 @@ let true_pattern = put_pat mmk "True" let and_pattern = put_pat mmk "(and ? ?)" let or_pattern = put_pat mmk "(or ? ?)" let eq_pattern = put_pat mmk "(eq ? ? ?)" -let pi_pattern = put_pat mmk "(x:?)((?)@[x])" -let imply_pattern = put_pat mmk "?1->?2" +let pi_pattern = put_pat mmk "(x : ?)((?)@[x])" +let imply_pattern = put_pat mmk "?1 -> ?2" let iff_pattern = put_pat mmk "(iff ? ?)" let not_pattern = put_pat mmk "(not ?1)" let mkIMP a b = soinstance imply_pattern [a;b] @@ -120,7 +120,7 @@ let dyck_imply_intro = (dImp None) -------------- A->B,A,Gamma |- G (A Atomique) *) -let atomic_imply_bot_pattern = put_pat mmk "?1->?2" +let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2" let atomic_imply_step cls gls = let mvb = somatch (clause_type cls gls) atomic_imply_bot_pattern in @@ -190,7 +190,7 @@ let back_thru_1 id = let exact_last_hyp = onLastHyp (fun h -> exact (VAR (out_some h))) -let imply_imply_bot_pattern = put_pat mmk "(?1->?2)->?3" +let imply_imply_bot_pattern = put_pat mmk "(?1 -> ?2) -> ?3" let imply_imply_step cls gls = let h0 = out_some cls in (* (C->D)->B *) |