From 09d156a3f1ee9ebaccc9dc971734aa94509ca51a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 24 Feb 2004 15:22:16 +0000 Subject: [PATCH] More V8.0 uris. --- .../content_expressions.ml | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 4d0708ae5..5fe5bc3dc 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -232,48 +232,48 @@ Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI (* 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));; -- 2.39.2