diff options
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 5968199359..2514b6e754 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -24,7 +24,7 @@ val new_meta : unit -> int (* [exist_to_meta] generates new metavariables for each existential and performs the replacement in the given constr *) val exist_to_meta : - Evd.evar_map -> (Evd.evar_map * constr) -> + Evd.evar_map -> Pretyping.open_constr -> ((int * types) list * constr) (* The Type of Constructions clausale environments. *) |