Bug fixed: the generated elimination principles used to have Anonymous

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index c204adf06457e91ff897b53130ace40e8f8e600c..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 ())
@@ -523,8 +523,8 @@ let eval_command status cmd =
      match obj with
         Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
          let name = UriManager.name_of_uri uri in
-        if not(CicPp.check name ty) then
-           MatitaLog.error ("Bad name: "^name);
+         if not(CicPp.check name ty) then
+           MatitaLog.warn ("Bad name: " ^ name);
          assert (metasenv = metasenv');
          let goalno =
           match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in