From bd2cbc7cbf6b0e06a1f588d1a426c83e40d9449b Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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 @@ lemma fact remark + variant 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