Added module DiscriminationTactics with brand new tactics Injection and

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index f7a0ab2e877a36c3e851fc45f4f57ad69a47c17d..e5e8469824226e37c5a2c013345f5e8d17c7d879 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -25,6 +25,7 @@
 
 exception Impossible of int;;
 exception NotRefinable of string;;
+exception Uncertain of string;;
 exception WrongUriToConstant of string;;
 exception WrongUriToVariable of string;;
 exception WrongUriToMutualInductiveDefinitions of string;;
@@ -291,6 +292,12 @@ and type_of_aux' metasenv context t =
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)
          C.Sort C.Type,subst',metasenv'
+     | (C.Meta _,_)
+     | (_,C.Meta _) ->
+       raise
+        (Uncertain
+          ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
+           CicPp.ppterm t2''))
      | (_,_) ->
        raise
         (NotRefinable
@@ -310,6 +317,10 @@ and type_of_aux' metasenv context t =
          in
           CicReduction.fdebug := -1 ;
           eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
+      | Cic.Meta _ as t ->
+         raise
+          (Uncertain
+            ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
       | _ -> raise (NotRefinable "Appl: wrong Prod-type")
     )
  in