From bd2cbc7cbf6b0e06a1f588d1a426c83e40d9449b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 8 Jul 2005 14:09:34 +0000
Subject: [PATCH] added variant thm flavour

---
 helm/matita/matita.lang     | 1 +
 helm/matita/matitaEngine.ml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

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 ())
-- 
2.39.2