diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-19 08:44:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-19 08:44:37 +0000 |
| commit | 34d8d8129e97db95334b5dce4843f89f1a052f53 (patch) | |
| tree | 89bed20205f7448b1698715fea6b30eea0a079b8 /proofs | |
| parent | 0f412d6ac5338e66ceee5f46acde922e4bb154be (diff) | |
reparation de make doc (ocamlweb & _)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2321 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 4138a49c3..f0c677cb3 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -48,8 +48,8 @@ val extract_decl : evar -> named_context sigma -> named_context sigma val restore_decl : evar -> evar_info -> named_context sigma -> named_context sigma -(* val w_Focusing_THEN : - evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic *) +(*i val w_Focusing_THEN : + evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic i*) val w_Declare : evar -> types -> w_tactic val w_Define : evar -> constr -> w_tactic |