diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-08 19:02:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:26 +0100 |
| commit | 85ab3e298aa1d7333787c1fa44d25df189ac255c (patch) | |
| tree | 32f661f4ccd3fb36657bb9ac8104a08df9cd1d87 /pretyping/evardefine.mli | |
| parent | 67dc22d8389234d0c9b329944ff579e7056b7250 (diff) | |
Pretyping API using EConstr.
Diffstat (limited to 'pretyping/evardefine.mli')
| -rw-r--r-- | pretyping/evardefine.mli | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index f7bf4636b..9c03a6e3f 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -8,6 +8,7 @@ open Names open Term +open EConstr open Evd open Environ @@ -18,16 +19,16 @@ type type_constraint = types option type val_constraint = constr option val empty_tycon : type_constraint -val mk_tycon : EConstr.constr -> type_constraint +val mk_tycon : constr -> type_constraint val empty_valcon : val_constraint -val mk_valcon : EConstr.constr -> val_constraint +val mk_valcon : constr -> val_constraint (** Instantiate an evar by as many lambda's as needed so that its arguments are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into [?y[vars1:=args1,vars:=args]] with [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *) -val evar_absorb_arguments : env -> evar_map -> EConstr.existential -> EConstr.constr list -> - evar_map * EConstr.existential +val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> + evar_map * existential val split_tycon : Loc.t -> env -> evar_map -> type_constraint -> @@ -36,9 +37,9 @@ val split_tycon : val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : int -> type_constraint -> type_constraint -val define_evar_as_product : evar_map -> EConstr.existential -> evar_map * EConstr.types -val define_evar_as_lambda : env -> evar_map -> EConstr.existential -> evar_map * EConstr.types -val define_evar_as_sort : env -> evar_map -> EConstr.existential -> evar_map * sorts +val define_evar_as_product : evar_map -> existential -> evar_map * types +val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types +val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts (** {6 debug pretty-printer:} *) |