diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-02-15 18:36:56 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-02-15 18:36:56 +0100 |
commit | 4a2db61b8f59a2871de4f4b69522193ff9440261 (patch) | |
tree | aed51f7e320c57e665748dbae973929725f3cee7 /src/trace/coqInterface.ml | |
parent | 3e5897710dc45c1b0bede79d3d61f4211c5ccb0e (diff) | |
parent | 23ac3ceceb92cdbc2026253c1bae388a2b9b6e18 (diff) | |
download | smtcoq-4a2db61b8f59a2871de4f4b69522193ff9440261.tar.gz smtcoq-4a2db61b8f59a2871de4f4b69522193ff9440261.zip |
Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13
Diffstat (limited to 'src/trace/coqInterface.ml')
-rw-r--r-- | src/trace/coqInterface.ml | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml index f11563c..a3dc327 100644 --- a/src/trace/coqInterface.ml +++ b/src/trace/coqInterface.ml @@ -92,41 +92,13 @@ type econstr = EConstr.t let econstr_of_constr = EConstr.of_constr -(* Modules *) -let gen_constant_in_modules s m n = - (* UnivGen.constr_of_monomorphic_global will crash on universe polymorphic constants *) - UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n -let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) -let init_modules = Coqlib.init_modules - - (* Int63 *) -let int63_module = [["Coq";"Numbers";"Cyclic";"Int63";"Int63"]] - let mkInt : int -> Constr.constr = fun i -> Constr.mkInt (Uint63.of_int i) -let cint = gen_constant int63_module "int" - (* PArray *) -let parray_modules = [["SMTCoq";"PArray";"PArray"]] - -let cmake = gen_constant parray_modules "make" -let cset = gen_constant parray_modules "set" - let max_array_size : int = 4194302 -let mkArray : Constr.types * Constr.t array -> Constr.t = - fun (ty, a) -> - let l = (Array.length a) - 1 in - snd (Array.fold_left (fun (i,acc) c -> - let acc' = - if i = l then - acc - else - mkApp (Lazy.force cset, [|ty; acc; mkInt i; c|]) in - (i+1,acc') - ) (0, mkApp (Lazy.force cmake, [|ty; mkInt l; a.(l)|])) a) (* Traces *) @@ -147,10 +119,6 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = module Micromega_plugin_Micromega = Micromega_plugin.Micromega module Micromega_plugin_Certificate = Micromega_plugin.Certificate -let micromega_coq_proofTerm = - (* Cannot contain evars *) - lazy (gen_constant_in_modules "ZMicromega" [["Coq"; "micromega";"ZMicromega"]] "ZArithProof") - let micromega_dump_proof_term p = (* Cannot contain evars *) EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) |