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 ba8ae7d98cd04606ee60fa7cf779f333482e0eca..04f32eb2c77aaddf3ce18896f93cf6e9f95c497a 100644 (file)
--- 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"