diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-21 17:24:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-21 17:24:37 +0000 |
| commit | b7af7027d15afa2dee1695792a2658f0df392956 (patch) | |
| tree | bebcce8f9fbb305d0bd9aa203ec843677665323b /tactics | |
| parent | accec4fc961d85ef21e73e690dedc36ce4c25f46 (diff) | |
Compatibilité ocamlweb pour cible doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.mli | 8 | ||||
| -rw-r--r-- | tactics/evar_tactics.mli | 4 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 2 | ||||
| -rw-r--r-- | tactics/extratactics.mli | 2 | ||||
| -rw-r--r-- | tactics/setoid_replace.mli | 8 |
5 files changed, 12 insertions, 12 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index f511fe675..4afdfe757 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -30,8 +30,8 @@ val general_rewrite_bindings : bool -> constr with_bindings -> tactic val general_rewrite : bool -> constr -> tactic (* Obsolete, use [general_rewrite_bindings l2r] -val rewriteLR_bindings : constr with_bindings -> tactic -val rewriteRL_bindings : constr with_bindings -> tactic +[val rewriteLR_bindings : constr with_bindings -> tactic] +[val rewriteRL_bindings : constr with_bindings -> tactic] *) (* Equivalent to [general_rewrite l2r] *) @@ -94,8 +94,8 @@ val substHyp : bool -> types -> identifier -> tactic (which, if they fail, raise only UserError, not PatternMatchingFailure) or [substClause lr (mkVar id) None] or [substClause lr (mkVar id) (Some hyp)] -val hypSubst_LR : identifier -> clause -> tactic -val hypSubst_RL : identifier -> clause -> tactic +[val hypSubst_LR : identifier -> clause -> tactic] +[val hypSubst_RL : identifier -> clause -> tactic] *) val discriminable : env -> evar_map -> constr -> constr -> bool diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 7d9a32380..89c5e58b8 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -15,8 +15,8 @@ open Tacexpr val instantiate : int -> Rawterm.rawconstr -> (identifier * hyp_location_flag, unit) location -> tactic -(* +(*i val instantiate_tac : tactic_arg list -> tactic -*) +i*) val let_evar : name -> Term.types -> tactic diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index ec3a990ac..cc1db7eb3 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Tacexpr open Term diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 34da41ebb..9431a6871 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Names open Term diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 426ff6edd..09fb39da8 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Term open Proof_type @@ -25,8 +25,8 @@ type relation = } type 'a relation_class = - Relation of 'a (* the rel_aeq of the relation or the relation*) - | Leibniz of constr option (* the carrier (if eq is partially instantiated)*) + Relation of 'a (* the [rel_aeq] of the relation or the relation*) + | Leibniz of constr option (* the [carrier] (if [eq] is partially instantiated)*) type 'a morphism = { args : (bool option * 'a relation_class) list; @@ -47,7 +47,7 @@ val print_setoids : unit -> unit val equiv_list : unit -> constr list val default_relation_for_carrier : ?filter:(relation -> bool) -> types -> relation relation_class -(* [default_morphism] raises Not_found *) +(* [default_morphism] raises [Not_found] *) val default_morphism : ?filter:(constr morphism -> bool) -> constr -> relation morphism |