From b3769ff3eb77ec8fa27ac46ec1076941a16bd3a5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Feb 2004 14:22:11 +0000 Subject: [PATCH] Bug fixed: when a variable not instantiated yet was restricted, some nececssary restrictions were not performed due to a typo. --- helm/ocaml/cic_unification/cicMetaSubst.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index ba8ae7d98..04f32eb2c 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -205,7 +205,7 @@ let rec restrict subst to_be_restricted metasenv = "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" n (names_of_context_indexes context to_be_restricted) n (CicPp.ppterm s))) - with Not_found -> (more @ more_to_be_restricted, metasenv', subst)) + with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst)) with Occur -> raise (MetaSubstFailure (sprintf "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" -- 2.39.2