diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 20:11:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 20:38:41 +0100 |
| commit | e98d7276f52c4b67bf05a80a6b44f334966f82fd (patch) | |
| tree | e85396003f974d5eaa8f84722c0ca3f050990da1 /pretyping/evardefine.mli | |
| parent | 08c31f46aa05098e1a97d9144599c1e5072b7fc3 (diff) | |
Splitting Evarutil in two distinct files.
Some parts of Evarutils were related to the management of evars under constraints.
We put them in the Evardefine file.
Diffstat (limited to 'pretyping/evardefine.mli')
| -rw-r--r-- | pretyping/evardefine.mli | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli new file mode 100644 index 000000000..07b0e69d9 --- /dev/null +++ b/pretyping/evardefine.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Term +open Evd +open Environ + +val env_nf_evar : evar_map -> env -> env +val env_nf_betaiotaevar : evar_map -> env -> env + +type type_constraint = types option +type val_constraint = constr option + +val empty_tycon : type_constraint +val mk_tycon : constr -> type_constraint +val empty_valcon : 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 -> existential -> constr list -> + evar_map * existential + +val split_tycon : + Loc.t -> env -> evar_map -> type_constraint -> + evar_map * (Name.t * type_constraint * type_constraint) + +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 + +(** {6 debug pretty-printer:} *) + +val pr_tycon : env -> type_constraint -> Pp.std_ppcmds + |