(* zero and one *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
(fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
(fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
(* times *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "times",
- None, Some "cic:/Coq/Init/Peano/mult.con"))
+ None, Some HelmLibraryObjects.Peano.mult_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "times",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con"))
+ None, Some HelmLibraryObjects.Reals.rmult_SURI))
:: List.map acic2cexpr args));;
(* minus *)
-Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "minus",
- None, Some "cic:/Coq/Arith/Minus/mult.con"))
+ None, Some HelmLibraryObjects.Peano.minus_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "minus",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
+ None, Some HelmLibraryObjects.Reals.rminus_SURI))
:: List.map acic2cexpr args));;
(* div *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "div",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
+ None, Some HelmLibraryObjects.Reals.rdiv_SURI))
:: List.map acic2cexpr args));;
function
Cic.Prop -> "Prop"
| Cic.Set -> "Set"
- | Cic.Type -> "Type"
+ | Cic.Type _ -> "Type" (* TASSI *)
| Cic.CProp -> "Type"
;;
let get_constructors uri i =
let inductive_types =
- (match CicEnvironment.get_obj uri with
- Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
+ Cic.Constant _ -> assert false
+ | Cic.Variable _ -> assert false
+ | Cic.CurrentProof _ -> assert false
+ | Cic.InductiveDefinition (l,_,_) -> l
) in
let (_,_,_,constructors) = List.nth inductive_types i in
constructors
make_subst subst, Some uri_str)::List.map acic2cexpr tl))
| C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
let inductive_types =
- (match CicEnvironment.get_obj uri with
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| Cic.CurrentProof _ -> assert false
make_subst subst, Some (UriManager.string_of_uri uri)))
| C.AMutInd (id,uri,i,subst) ->
let inductive_types =
- (match CicEnvironment.get_obj uri with
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| Cic.CurrentProof _ -> assert false