- occur check test anticipated to the delift phase

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e3086c80126011c9a8be1bdb32a187e45c355296..54fde9a45a6d49c4d8e8d33ce88e98af2282f552 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -35,7 +35,6 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception RelToHiddenHypothesis;;
 exception MetasenvInconsistency;;
 exception MutCaseFixAndCofixRefineNotImplemented;;
-exception FreeMetaFound of int;;
 exception WrongArgumentNumber;;
 
 let fdebug = ref 0;;
@@ -111,7 +110,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
   let module C = Cic in
   let module R = CicMetaSubst in
   let module Un = CicUnification in 
-  match R.whd subst context expectedtype with
+  match R.whd metasenv subst context expectedtype with
      C.MutInd (_,_,_) ->
        (n,context,actualtype, [term]), subst, metasenv
    | C.Appl (C.MutInd (_,_,_)::tl) ->
@@ -120,7 +119,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
    | C.Prod (name,so,de) ->
       (* we expect that the actual type of the branch has the due 
          number of Prod *)
-      (match R.whd subst context actualtype with
+      (match R.whd metasenv subst context actualtype with
            C.Prod (name',so',de') ->
              let subst, metasenv = 
                 Un.fo_unif_subst subst context metasenv so so' in
@@ -162,12 +161,7 @@ and type_of_aux' metasenv context t =
        decr fdebug ;
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) =
-        try
-         List.find (function (m,_,_) -> n = m) metasenv
-        with
-         Not_found -> raise (FreeMetaFound n)
-       in
+       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         let subst',metasenv' =
          check_metasenv_consistency subst metasenv context canonical_context l
         in
@@ -267,7 +261,7 @@ and type_of_aux' metasenv context t =
             raise
              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
        let rec count_prod t =
-         match CicMetaSubst.whd subst context t with
+         match CicMetaSubst.whd metasenv subst context t with
              C.Prod (_, _, t) -> 1 + (count_prod t)
            | _ -> 0 in 
        let no_args = count_prod arity in
@@ -292,7 +286,7 @@ and type_of_aux' metasenv context t =
        let _, subst, metasenv =
          type_of_aux subst metasenv context expected_type
        in
-       let actual_type = CicMetaSubst.whd subst context actual_type in
+       let actual_type = CicMetaSubst.whd metasenv subst context actual_type in
        let subst,metasenv =
          Un.fo_unif_subst subst context metasenv expected_type actual_type
        in
@@ -342,11 +336,11 @@ and type_of_aux' metasenv context t =
                   type_of_aux subst metasenv context appl
                 in
 *)
-                CicMetaSubst.whd subst context appl
+                CicMetaSubst.whd metasenv subst context appl
               in
                Un.fo_unif_subst subst context metasenv instance instance')
              (subst,metasenv) outtypeinstances in
-        CicMetaSubst.whd subst
+        CicMetaSubst.whd metasenv subst
           context (C.Appl(outtype::right_args@[term])),subst,metasenv
    | C.Fix _
    | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
@@ -427,8 +421,10 @@ and type_of_aux' metasenv context t =
    let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
    let t1' = CicMetaSubst.apply_subst subst' t1 in
    let t2' = CicMetaSubst.apply_subst subst' t2 in
-    let t1'' = CicMetaSubst.whd subst' context t1' in
-    let t2'' = CicMetaSubst.whd subst' ((Some (name,C.Decl s))::context) t2' in
+    let t1'' = CicMetaSubst.whd metasenv subst' context t1' in
+    let t2'' =
+      CicMetaSubst.whd metasenv subst' ((Some (name,C.Decl s))::context) t2'
+    in
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
@@ -452,7 +448,7 @@ and type_of_aux' metasenv context t =
   function
      [] -> hetype,subst,metasenv
    | (hete, hety)::tl ->
-    (match (CicMetaSubst.whd subst context hetype) with
+    (match (CicMetaSubst.whd metasenv subst context hetype) with
         Cic.Prod (n,s,t) ->
          let subst',metasenv' =
            CicUnification.fo_unif_subst subst context metasenv s hety