}
let get_types uri =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
| Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno
| _ -> assert false
| Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
| Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
| Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
- | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
+ | Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
| Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
| Cic.AImplicit (id, _) -> idref id Ast.Implicit
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
| `Set | `Type _ -> `Pi
- | `Prop | `CProp -> `Forall
+ | `Prop | `CProp _ -> `Forall
in
idref id (Ast.Binder (binder_kind,
(CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
| Cic.ALambda (id,n,s,t) ->
idref id (Ast.Binder (`Lambda,
(CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
- | Cic.ALetIn (id,n,s,t) ->
- idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
+ | Cic.ALetIn (id,n,s,ty,t) ->
+ idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, Some (k ty)),
k s, k t))
| Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
let instantiate32 term_info idrefs env symbol args =
let rec instantiate_arg = function
| Ast.IdentArg (n, name) ->
- let t = (try List.assoc name env with Not_found -> assert false) in
+ let t =
+ try List.assoc name env
+ with Not_found -> prerr_endline ("name not found in env: "^name);
+ assert false
+ in
let rec count_lambda = function
| Ast.AttributedTerm (_, t) -> count_lambda t
| Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
ast, term_info.uri
+let counter = ref ~-1
+let reset () = counter := ~-1;;
let fresh_id =
- let counter = ref ~-1 in
fun () ->
incr counter;
!counter