diff options
author | ckeller <ckeller@users.noreply.github.com> | 2019-03-15 11:23:55 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-15 11:23:55 +0100 |
commit | ae455fa3aa29c872c9c5b2736fff861afebcd051 (patch) | |
tree | 1db2df3a7bd9ca076ea4007d59557a549af9dc04 /src/versions/standard/structures.ml | |
parent | 4a610de645ca2bb505c97dd082220a57595019ad (diff) | |
download | smtcoq-ae455fa3aa29c872c9c5b2736fff861afebcd051.tar.gz smtcoq-ae455fa3aa29c872c9c5b2736fff861afebcd051.zip |
V8.9 (#43)
* New syntax for implicit arguments
* Towards 8.9: problems with Micromega plugin
* Move to _CoqProject
* Back to name Makefile
* Switch to Makefile.local instead of -extra
* The compilation issue is a Coq bug
* Ok with 8.9
* INSTALL with 8.9
* Everything ok with 8.9
Diffstat (limited to 'src/versions/standard/structures.ml')
-rw-r--r-- | src/versions/standard/structures.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index f259a70..ea35a35 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -77,14 +77,14 @@ let mkTConst c noc ty = (* TODO : Set -> Type *) let declare_new_type t = - let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make t) in + let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in Constr.mkVar t let declare_new_variable v constr_t = let env = Global.env () in let evd = Evd.from_env env in let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in - let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make v) in + let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in Constr.mkVar v let declare_constant n c = @@ -103,7 +103,7 @@ let econstr_of_constr = EConstr.of_constr (* Modules *) -let gen_constant_in_modules s m n = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n +let gen_constant_in_modules s m n = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) @@ -165,18 +165,18 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = (* Micromega *) -module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils +module Micromega_plugin_Mutils = Mutils_full +module Micromega_plugin_Certificate = Micromega_plugin.Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega_full let micromega_coq_proofTerm = (* Cannot contain evars *) - lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin.Coq_micromega.M.coq_proofTerm))) + lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin_Coq_micromega.M.coq_proofTerm))) let micromega_dump_proof_term p = (* Cannot contain evars *) - EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) + EConstr.Unsafe.to_constr (Micromega_plugin_Coq_micromega.dump_proof_term p) (* Tactics *) |