From d70d83df962621feeb0e674810a1b9583c7e5487 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 21 Aug 2008 17:35:19 +0000 Subject: [PATCH] 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. --- helm/software/components/cic_unification/cicMetaSubst.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml index 91368cde9..6d187432a 100644 --- 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 -- 2.39.2