Added catching of an exception to implement a missing occur check:

when unifying ?1 : T with t : T', T and T' are unified first. If ?1
occurs in T', it is moved from the metasenv to the subst, and the
exception here used to escape.

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 91368cde95549c1fdc096561720ebee7e90dc442..6d187432ae12ba7e73789d4af25719eedc6e637e 100644 (file)
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -627,7 +627,14 @@ let delift n subst context metasenv l t =
 
  let module S = CicSubstitution in
   let l =
-   let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
+   let (_, canonical_context, _) =
+    try
+     CicUtil.lookup_meta n metasenv
+    with CicUtil.Meta_not_found _ ->
+     raise (MetaSubstFailure (lazy
+      ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^
+       "declared in the metasenv")))
+    in
    List.map2 (fun ct lt ->
      match (ct, lt) with
      | None, _ -> None