diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 03:04:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:31 +0100 |
| commit | d833b81b49366e95cf20a1d00f9c63883adb8942 (patch) | |
| tree | 1afca49fcd42e96b658c90d28e9da692ccc39724 /engine/evarutil.mli | |
| parent | c0d38ae52ac410811e7df54c52e8d3a18bb11bcb (diff) | |
Rewrite API using EConstr.
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 1b592b790..cf36f5953 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -52,8 +52,8 @@ val e_new_type_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> EConstr.constr * sorts -val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr +val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (EConstr.constr, 'r) Sigma.sigma +val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> EConstr.constr val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> constr list option -> (existential_key, 'r) Sigma.sigma |