diff options
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 623890538..203353876 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -87,8 +87,9 @@ val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic val clenv_independent : wc clausenv -> int list val clenv_missing : 'a clausenv -> int list +val clenv_constrain_missing_args : (* Used in user contrib Lannion *) + constr list -> wc clausenv -> wc clausenv (* -val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv *) val clenv_lookup_name : 'a clausenv -> identifier -> int |