diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 08:51:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 08:51:59 +0000 |
| commit | 33a25f335839886cc205946bdc198ebab3b386de (patch) | |
| tree | 7d76954f046caa73ff9880c97af2fdb24854aaee /proofs/evar_refiner.mli | |
| parent | e75373c73188d8fbcf7578a0578ce27d60c7b73f (diff) | |
Option pour rendre les vérifications du refiner optionnelle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/evar_refiner.mli')
| -rw-r--r-- | proofs/evar_refiner.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index b0dd5e4f4..55c7282c2 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -30,8 +30,6 @@ val rc_of_glsigma : goal sigma -> wc dependent goal *) type w_tactic = wc -> wc -val local_Constraints : tactic - val startWalk : goal sigma -> wc * (wc -> tactic) val extract_decl : evar -> w_tactic |