diff options
| author |  Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-11-30 19:14:17 +0000 |
|---|---|---|
| committer | Assia Mahboubi <assia.mahboubi@inria.fr> | 2007-11-30 19:14:17 +0000 |
| commit | 6056026627af61aaef081bd828fb0bc8c2869a91 (patch) | |
| tree | 1c76c5927afd6802295d6603e9acb176d91c39dd /coq/coq-syntax.el | |
| parent | 18701aef52d1510be5672a70df387ddb4d6b523a (diff) | |
coq solve tacs modified
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 9a405db5..88e32e30 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -193,7 +193,7 @@ so for the following reasons: ("compare" "cmpa" "compare # #" t "compare") ("compute" "cmpu" "compute" t "compute") ;; ("congruence" "cong" "congruence" t "congruence") -;; ("constructor" "cons" "constructor" t "constructor") + ("constructor" "cons" "constructor" t "constructor") ;; ("contradiction" "contr" "contradiction" t "contradiction") ("cut" "cut" "cut" t "cut") ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") @@ -217,7 +217,7 @@ so for the following reasons: ("eauto with arith" "eawa" "eauto with arith" t) ("eauto with" "eaw" "eauto with @{db}" t) ("eauto" "ea" "eauto" t "eauto") -;; ("econstructor" "econs" "econstructor" t "econstructor") + ("econstructor" "econs" "econstructor" t "econstructor") ("eexists" "eex" "eexists" t "eexists") ("eleft" "eleft" "eleft" t "eleft") ("elim using" "elu" "elim # using #" t) @@ -307,7 +307,7 @@ so for the following reasons: ("subst" "su" "subst #" t "subst") ("symmetry" "sy" "symmetry" t "symmetry") ("symmetry in" "syi" "symmetry in #" t) - ("tauto" "ta" "tauto" t "tauto") + ;; ("tauto" "ta" "tauto" t "tauto") ("transitivity" "trans" "transitivity #" t "transitivity") ("trivial" "t" "trivial" t "trivial") ("trivial with" "tw" "trivial with @{db}" t) @@ -326,11 +326,9 @@ so for the following reasons: ("assumption" "as" "assumption" t "assumption") ("by" "by" "by #" t "by") ("congruence" "cong" "congruence" t "congruence") - ("constructor" "cons" "constructor" t "constructor") ("contradiction" "contr" "contradiction" t "contradiction") ("decide equality" "deg" "decide equality" t "decide\\s-+equality") ("discriminate" "dis" "discriminate" t "discriminate") - ("econstructor" "econs" "econstructor" t "econstructor") ("exact" "exa" "exact" t "exact") ("fourier" "four" "fourier" t "fourier") ("fail" "fa" "fail" nil) @@ -338,6 +336,7 @@ so for the following reasons: ("omega" "o" "omega" t "omega") ("reflexivity" "refl" "reflexivity #" t "reflexivity") ("ring" "ring" "ring #" t "ring") + ("tauto" "ta" "tauto" t "tauto") )) "Coq tactic(al)s that solve a subgoal." ) |