diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-05 20:13:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:23:51 +0100 |
| commit | 147afe827dc83602cc160a8b1357e84ecea910ff (patch) | |
| tree | 3c38de92215152d4de4c4a5ba57e217cc8e0f293 /pretyping/evardefine.mli | |
| parent | 83607f75a13ea915affa8cfc5bfc14cc944c61ef (diff) | |
Evardefine API using EConstr.
Diffstat (limited to 'pretyping/evardefine.mli')
| -rw-r--r-- | pretyping/evardefine.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 07b0e69d9..f6d0efba6 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -18,15 +18,15 @@ type type_constraint = types option type val_constraint = constr option val empty_tycon : type_constraint -val mk_tycon : constr -> type_constraint +val mk_tycon : EConstr.constr -> type_constraint val empty_valcon : val_constraint -val mk_valcon : constr -> val_constraint +val mk_valcon : EConstr.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 -> existential -> constr list -> +val evar_absorb_arguments : env -> evar_map -> EConstr.existential -> EConstr.constr list -> evar_map * existential val split_tycon : @@ -36,9 +36,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 -> 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 +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 (** {6 debug pretty-printer:} *) |