diff options
| -rw-r--r-- | proofs/clenv.ml | 3 | ||||
| -rw-r--r-- | proofs/clenv.mli | 3 |
2 files changed, 5 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 6db3cfcac4..6291c2328e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -932,6 +932,9 @@ let clenv_constrain_dep_args hyps_only clause = function error ("Not the right number of missing arguments (expected " ^(string_of_int (List.length occlist))^")") +let clenv_constrain_missing_args mlist clause = + clenv_constrain_dep_args true clause mlist + let clenv_lookup_name clenv id = match intmap_inv clenv.namenv id with | [] -> diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 6238905389..2033538761 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 |