diff options
| author | msozeau | 2008-01-18 00:12:05 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-18 00:12:05 +0000 |
| commit | 72dccfa0f5edb59b1ba2668e91828742ab91bb1d (patch) | |
| tree | 46339464eee6a725dc9ae10d38bd8ae45e724e44 /parsing | |
| parent | edbb81e324234548c2bb70306fb448420e1bbd70 (diff) | |
Change notation for setoid inequality, coerce objects before comparing them. Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 3 |
2 files changed, 0 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b69a6a97ac..dacfd7329a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -495,9 +495,6 @@ GEXTEND Gram | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is - | IDENT "Instantiation"; IDENT "Tactic"; ":="; tac = Tactic.tactic -> - VernacSetInstantiationTactic tac - (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; enrich = [ IDENT "Enriching" -> true | -> false ]; (local,qid,pos) = diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index e2653a9606..3502a9e86c 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -717,9 +717,6 @@ let rec pr_vernac = function | VernacDeclareInstance id -> hov 1 (str"Instance" ++ spc () ++ pr_lident id) - | VernacSetInstantiationTactic tac -> - hov 1 (str"Instantiation Tactic :=" ++ spc () ++ pr_raw_tactic tac) - (* Modules and Module Types *) | VernacDefineModule (export,m,bl,ty,bd) -> let b = pr_module_binders_list bl pr_lconstr in |