Bug fixed: the current substitution and metasenv were not propagated to the

check_allowed_sort_elimination function. As a result:
 1. useless metas were opened by the apply tactic
 2. sometimes unification failed

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 18de8af5e22047e54a668519cf997aa556f7c34b..b24c5fc8e7b2b4e3cd50074a2bb1560220445c72 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1263,16 +1263,18 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
              args coInductiveTypeURI
          ) fl true
 
-and check_allowed_sort_elimination ~logger context uri i need_dummy ind 
-  arity1 arity2 ugraph =
+and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+  need_dummy ind arity1 arity2 ugraph =
  let module C = Cic in
  let module U = UriManager in
-  match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
+  match (CicReduction.whd ~subst context arity1, CicReduction.whd ~subst context arity2) with
      (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
-       let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in
+       let b,ugraph1 =
+        CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
        if b then
-        check_allowed_sort_elimination ~logger context uri i need_dummy
-           (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
+        check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+          need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
+          ugraph1
        else
         false,ugraph1
    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
@@ -1322,11 +1324,12 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
      (* TASSI: da verificare *)
    | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
-       let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
+       let b,ugraph1 =
+        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
        if not b then
         false,ugraph1
        else
-         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
+         (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
               C.Sort C.Prop -> true,ugraph1
            | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
                (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -1343,11 +1346,12 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
    | ((C.Sort C.Set, C.Prod (name,so,ta)) 
    | (C.Sort C.CProp, C.Prod (name,so,ta)))
      when not need_dummy ->
-       let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
+       let b,ugraph1 =
+        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
        if not b then
         false,ugraph1
        else
-         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
+         (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
            C.Sort C.Prop
          | C.Sort C.Set  -> true,ugraph1
          | C.Sort C.CProp -> true,ugraph1
@@ -1377,7 +1381,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
          )
    | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
        (* TASSI: da verificare *)
-       CicReduction.are_convertible context so ind ugraph
+       CicReduction.are_convertible ~subst ~metasenv context so ind ugraph
    | (_,_) -> false,ugraph
         
 and type_of_branch context argsno need_dummy outtype term constype =
@@ -1741,8 +1745,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       let type_of_sort_of_ind_ty,ugraph3 = 
        type_of_aux ~logger context sort_of_ind_type ugraph2 in
       let b,ugraph4 = 
-       check_allowed_sort_elimination ~logger  context uri i need_dummy
-         sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3 
+       check_allowed_sort_elimination ~subst ~metasenv ~logger  context uri i
+          need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3 
       in
        if not b then
         raise