bugfix: FreshNameGenerator uses the type checker on mk_fresh_name

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5d3d40a106f3c7af6db019e2021cafc54014ad44..be7c4b0d0aeaca45b0dc26704bf92a3dde6032c5 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1005,7 +1005,12 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
       let consty =
-       match CicEnvironment.get_cooked_obj ~trust:false uri with
+       let obj =
+         try
+           CicEnvironment.get_cooked_obj ~trust:false uri
+         with Not_found -> assert false
+       in
+       match obj with
           C.InductiveDefinition (itl,_,_) ->
            let (_,_,_,cl) = List.nth itl i in
             let (_,cons) = List.nth cl (j - 1) in
@@ -1537,7 +1542,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t =
           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
         (* let's check if the type of branches are right *)
       let parsno =
-        match CicEnvironment.get_cooked_obj ~trust:false uri with
+        let obj =
+          try
+            CicEnvironment.get_cooked_obj ~trust:false uri
+          with Not_found -> assert false
+        in
+        match obj with
             C.InductiveDefinition (_,_,parsno) -> parsno
           | _ ->
               raise (TypeCheckerFailure
@@ -1727,7 +1737,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t =
    match CicReduction.whd context ty with
       C.MutInd (uri,i,_) ->
        (*CSC: definire una funzioncina per questo codice sempre replicato *)
-       (match CicEnvironment.get_cooked_obj ~trust:false uri with
+        let obj =
+          try
+            CicEnvironment.get_cooked_obj ~trust:false uri
+          with Not_found -> assert false
+        in
+        (match obj with
            C.InductiveDefinition (itl,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
              if is_inductive then None else (Some uri)
@@ -1848,7 +1863,7 @@ let typecheck uri =
 
 let type_of_aux' ?(subst = []) metasenv context t =
   let logger = new CicLogger.logger in
-  type_of_aux' ~logger metasenv context t
+  type_of_aux' ~logger ~subst metasenv context t
 
 let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
   let logger = new CicLogger.logger in