From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 8 Jul 2005 14:09:34 +0000 (+0000)
Subject: added variant thm flavour
X-Git-Tag: pre_notation~67
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bd2cbc7cbf6b0e06a1f588d1a426c83e40d9449b;p=helm.git

added variant thm flavour
---

diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index 0fac57ec9..d01280c90 100644
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -20,6 +20,7 @@
     <keyword>lemma</keyword>
     <keyword>fact</keyword>
     <keyword>remark</keyword>
+    <keyword>variant</keyword>
   </keyword-list>
     
   <keyword-list _name = "Commands" style = "Keyword" case-sensitive="TRUE">
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 354ecd9e8..c5b2fb987 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -410,7 +410,7 @@ let disambiguate_obj status obj =
     | TacticAst.Record (_,name,_,_) ->
        Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
     | TacticAst.Inductive _ -> assert false
-    | _ -> None in
+    | TacticAst.Theorem _ -> None in
   let (aliases, metasenv, cic, _) =
     match
       MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())