Elim generalized to saturate its argument.

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index ebcf0538ac75030c6e71e9fffc961d3e5d2ccafd..354ecd9e819424cccf20424c31f99604a0252212 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -522,6 +522,9 @@ let eval_command status cmd =
      let metasenv = MatitaMisc.get_proof_metasenv status in
      match obj with
         Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
+         let name = UriManager.name_of_uri uri in
+         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