diff options
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) -> |