diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-12 06:45:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-12 06:45:13 +0000 |
| commit | c233719254afe853f796113d8bd5c087944abdaa (patch) | |
| tree | ce1df6ffb09af271278bfbe52d23b68239c5779a /proofs | |
| parent | 38398456ebae7069569fe97f20796ebfb8aee8de (diff) | |
Re-introduction de clenv_constrain_missing_arg utilisé par la contrib Lannion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -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 6db3cfcac..6291c2328 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 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 |