V8.8 (#42)

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Organization structures

* 8.8 ok with standard coq

1 files changed, 82 insertions, 61 deletions

diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 3d17203..3d6f6b2 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -10,74 +10,80 @@
 (**************************************************************************)
 
 
-(* Constr generation and manipulation *)
 (* WARNING: currently, we map all the econstr into constr: we suppose
    that the goal does not contain existencial variables *)
-val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
-val gen_constant : string list list -> string -> Term.constr lazy_t
+
+(* Constr generation and manipulation *)
+type id = Names.variable
+val mkId : string -> id
+
+type name
+val name_of_id : id -> name
+val mkName : string -> name
+val string_of_name : name -> string
+
+type constr = Constr.t
+type types = constr
+val eq_constr : constr -> constr -> bool
+val hash_constr : constr -> int
+val mkProp : types
+val mkConst : Names.Constant.t -> constr
+val mkVar : id -> constr
+val mkRel : int -> constr
+val isRel : constr -> bool
+val destRel : constr -> int
+val lift : int -> constr -> constr
+val mkApp : constr * constr array -> constr
+val decompose_app : constr -> constr * constr list
+val mkLambda : name * types * constr -> constr
+val mkProd : name * types * types -> types
+val mkLetIn : name * constr * types * constr -> constr
+
+val pr_constr_env : Environ.env -> constr -> Pp.t
+val pr_constr : constr -> Pp.t
+
+val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry
+val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry
+val declare_new_type : id -> types
+val declare_new_variable : id -> types -> constr
+val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+
+type cast_kind
+val vmcast : cast_kind
+val mkCast : constr * cast_kind * constr -> constr
+
+
+(* EConstr *)
+type econstr = EConstr.t
+val econstr_of_constr : constr -> econstr
+
+
+(* Modules *)
+val gen_constant : string list list -> string -> constr lazy_t
+
 
 (* Int63 *)
 val int63_modules : string list list
-val int31_module : string list list
-val cD0 : Term.constr lazy_t
-val cD1 : Term.constr lazy_t
-val cI31 : Term.constr lazy_t
-val mkInt : int -> Term.constr
-val cint : Term.constr lazy_t
+val mkInt : int -> constr
+val cint : constr lazy_t
+
 
 (* PArray *)
 val parray_modules : string list list
-val cmake : Term.constr lazy_t
-val cset : Term.constr lazy_t
 val max_array_size : int
-val mkArray : Term.types * Term.constr array -> Term.constr
+val mkArray : types * constr array -> constr
+
 
 (* Traces *)
 val mkTrace :
-  ('a -> Term.constr) ->
+  ('a -> constr) ->
   ('a -> 'a) ->
   'b ->
-  Term.constr Lazy.t ->
-  Term.constr Lazy.t ->
-  Term.constr Lazy.t ->
-  Term.constr Lazy.t ->
-  int -> Term.constr -> Term.constr -> 'a ref -> Term.constr
-
-(* Differences between the two versions of Coq *)
-val mkUConst :
-  Term.constr -> Safe_typing.private_constants Entries.definition_entry
-val mkTConst :
-  Term.constr ->
-  Term.constr ->
-  Term.types -> Safe_typing.private_constants Entries.definition_entry
-val error : string -> 'a
-val coqtype : Term.types Future.computation
-val declare_new_type : Names.variable -> Term.constr
-val declare_new_variable : Names.variable -> Term.constr -> Term.constr
-val extern_constr : Term.constr -> Constrexpr.constr_expr
-val vernacentries_interp : Constrexpr.constr_expr -> unit
-val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
-val lift : int -> Constr.constr -> Constr.constr
-val destruct_rel_decl : Context.Rel.Declaration.t -> Names.Name.t * Constr.t
-val interp_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Term.constr
-val tclTHEN :
-  unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
-val tclTHENLAST :
-  unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
-val assert_before : Names.Name.t -> Term.types -> unit Proofview.tactic
-
-val vm_conv : Reduction.conv_pb -> Term.types Reduction.kernel_conversion_function
-val vm_cast_no_check : Term.constr -> unit Proofview.tactic
-val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr
-
-val mk_tactic :
-  (Environ.env -> Evd.evar_map -> Term.constr -> unit Proofview.tactic) ->
-  unit Proofview.tactic
-val set_evars_tac : Term.constr -> unit Proofview.tactic
-val ppconstr_lsimpleconstr : Ppconstr.precedence
-val constrextern_extern_constr : Term.constr -> Constrexpr.constr_expr
-val get_rel_dec_name : Context.Rel.Declaration.t -> Names.Name.t
-val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
+  constr Lazy.t ->
+  constr Lazy.t ->
+  constr Lazy.t ->
+  constr Lazy.t ->
+  int -> constr -> constr -> 'a ref -> constr
 
 
 (* Micromega *)
@@ -86,15 +92,30 @@ module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
 module Micromega_plugin_Micromega = Micromega_plugin.Micromega
 module Micromega_plugin_Mutils = Micromega_plugin.Mutils
 
-val micromega_coq_proofTerm : Term.constr lazy_t
-val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr
+val micromega_coq_proofTerm : constr lazy_t
+val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr
 
 
-(* Types in the Coq source code *)
+(* Tactics *)
 type tactic = unit Proofview.tactic
-type names_id = Names.Id.t
+val tclTHEN : tactic -> tactic -> tactic
+val tclTHENLAST : tactic -> tactic -> tactic
+val assert_before : name -> types -> tactic
+val vm_cast_no_check : constr -> tactic
+val mk_tactic : (Environ.env -> Evd.evar_map -> constr -> tactic) -> tactic
+val set_evars_tac : constr -> tactic
+
+
+(* Other differences between the two versions of Coq *)
 type constr_expr = Constrexpr.constr_expr
+val error : string -> 'a
+val extern_constr : constr -> constr_expr
+val destruct_rel_decl : Context.Rel.Declaration.t -> name * constr
+val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr
+val ppconstr_lsimpleconstr : Notation_term.tolerability
+val constrextern_extern_constr : constr -> constr_expr
+val get_rel_dec_name : Context.Rel.Declaration.t -> name
+val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr
 
-(* EConstr *)
-type econstr = EConstr.t
-val econstr_of_constr : Term.constr -> econstr
+val vm_conv : Reduction.conv_pb -> types Reduction.kernel_conversion_function
+val cbv_vm : Environ.env -> constr -> types -> constr