support for terms with metas in check

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

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index b46aa0b226516bcc8abab2bb9be679ef3583c435..b85a4a519a01cbd95dc77438cdd0a5a555f2b820 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -193,12 +193,6 @@ function
       Cic.Lambda (fresh_binder true,
         CicSubstitution.lift_from (rightno + 1) liftno indty, case)
 
-let string_of_sort = function
-  | Cic.Prop -> "Prop"
-  | Cic.CProp -> "CProp"
-  | Cic.Set -> "Set"
-  | Cic.Type _ -> "Type"
-
 let rec branch (uri, typeno) insource paramsno t fix head args =
   match t with
   | Cic.MutInd (uri', typeno', []) when
@@ -247,9 +241,9 @@ let branch (uri, typeno) insource liftno paramsno t fix head args =
   branch (uri, typeno) insource paramsno t fix head args
 
 let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
-  let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
+  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
   match obj with
-  | Cic.InductiveDefinition (indTypes, params, leftno) ->
+  | Cic.InductiveDefinition (indTypes, params, leftno, _) ->
       let (name, inductive, ty, constructors) =
         try
           List.nth indTypes typeno
@@ -346,8 +340,6 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
 prerr_endline (CicPp.ppterm eliminator_type);
 prerr_endline (CicPp.ppterm eliminator_body);
 *)
-prerr_endline "generato l'eliminatore";
-prerr_endline "inizio type checking";
       let (computed_type, ugraph) =
         try
           CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
@@ -356,8 +348,6 @@ prerr_endline "inizio type checking";
             "type checker failure while type checking:\n%s\nerror:\n%s"
             (CicPp.ppterm eliminator_body) msg))
       in
-prerr_endline "fine type checking";
-prerr_endline "inizio are convertible";
       if not (fst (CicReduction.are_convertible []
         eliminator_type computed_type ugraph))
       then
@@ -372,6 +362,9 @@ prerr_endline "inizio are convertible";
         | _ -> assert false
       in
       let name = UriManager.name_of_uri uri ^ suffix in
-      Cic.Constant (name, Some eliminator_body, eliminator_type, [])
-  | _ -> assert false
+      let obj_attrs = [`Class (`Elim sort); `Generated] in
+      Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs)
+  | _ ->
+      failwith (sprintf "not an inductive definition (%s)"
+        (UriManager.string_of_uri uri))