diff options
| author | filliatr | 2000-07-25 17:29:20 +0000 |
|---|---|---|
| committer | filliatr | 2000-07-25 17:29:20 +0000 |
| commit | c330f60f1617afcb42cebe2fd2ccf9f330ea4f89 (patch) | |
| tree | 53e61f40e19ea35216091af7324a6bbd4fc7e4bd /tactics | |
| parent | 968d65c616127446c5f1c5d3485e9efdc420e6a4 (diff) | |
retablissement make doc et make minicoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@571 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacentries.mli | 2 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 8 |
2 files changed, 6 insertions, 4 deletions
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli index 6efd48d555..b364706ca1 100644 --- a/tactics/tacentries.mli +++ b/tactics/tacentries.mli @@ -15,7 +15,7 @@ val v_symmetry : tactic_arg list -> tactic val v_transitivity : tactic_arg list -> tactic val v_intro : tactic_arg list -> tactic val v_introsUntil : tactic_arg list -> tactic -(*val v_tclIDTAC : tactic_arg list -> tactic*) +(*i val v_tclIDTAC : tactic_arg list -> tactic i*) val v_assumption : tactic_arg list -> tactic val v_exact : tactic_arg list -> tactic val v_reduce : tactic_arg list -> tactic diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 0cdedd8c68..4b89938276 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -37,8 +37,10 @@ val tclLAST_HYP : (constr -> tactic) -> tactic val tclTRY_sign : (constr -> tactic) -> var_context -> tactic val tclTRY_HYPS : (constr -> tactic) -> tactic -(*val dyn_tclIDTAC : tactic_arg list -> tactic -val dyn_tclFAIL : tactic_arg list -> tactic*) +(*i +val dyn_tclIDTAC : tactic_arg list -> tactic +val dyn_tclFAIL : tactic_arg list -> tactic +i*) (*s Clause tacticals. *) @@ -103,7 +105,7 @@ type branch_assumptions = { indargs : identifier list} (* the inductive arguments *) val sort_of_goal : goal sigma -> sorts -(*val suff : goal sigma -> constr -> string*) +(*i val suff : goal sigma -> constr -> string i*) val general_elim_then_using : constr -> (inductive -> int -> bool list) -> |