From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Feb 2004 14:22:11 +0000 (+0000)
Subject: Bug fixed: when a variable not instantiated yet was restricted, some
X-Git-Tag: V_0_2_3~72
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b3769ff3eb77ec8fa27ac46ec1076941a16bd3a5;p=helm.git

Bug fixed: when a variable not instantiated yet was restricted, some
nececssary restrictions were not performed due to a typo.
---

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"