added variant thm flavour

diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index 0fac57ec97e69a226e59498c7464650267821367..d01280c90535da579fef8c2e82831569a7d8f8dc 100644 (file)
--- 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 354ecd9e819424cccf20424c31f99604a0252212..c5b2fb98774702ee955193f6872a191240cea8a8 100644 (file)
--- 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 ())