From bae7532aaf4fc4ca0f637cb6e53f6b4b80c7cb75 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 3 May 2000 20:44:42 +0000
Subject: diverses modifs pour ocamlweb

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/hipattern.mli | 7 ++++---
 tactics/tacticals.mli | 4 ++--
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3ec63908fe..0161343071 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -63,7 +63,8 @@ val get_pat            : marked_pattern -> constr_pattern
 
 type marked_term
 val put_squel          : module_mark -> string -> marked_term
-(*val get_squel          : marked_term -> constr*)
+
+(*i val get_squel          : marked_term -> constr i*)
 
 (*i Remplacé par Astterm.interp_constrpattern
 val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr
@@ -98,7 +99,7 @@ val get_reference : string list -> string -> constr
 (* [dest_somatch c pat] matches [c] against [pat] and returns the resulting
    assignment of metavariables; it raises [PatternMatchingFailure] if
    not matchable *)
-(*
+(*i
 val dest_somatch : constr -> marked_pattern -> constr list
 
 (* [somatches c pat] just tells if [c] matches against [pat] *)
@@ -117,7 +118,7 @@ val dest_somatch_conv :
 
 val somatches_conv :
   Environ.env -> 'a evar_map -> constr -> marked_pattern -> bool
-*)
+i*)
 
 val soinstance   : marked_term -> constr list -> constr 
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ae38c210e4..de91973d62 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -48,10 +48,10 @@ val tclTHEN_i1     : tactic -> (int -> tactic) -> tactic
 val nth_clause  : int -> goal sigma -> clause
 val clause_type : clause -> goal sigma -> constr
 
-(*
+(*i
 val matches      : goal sigma -> constr -> marked_term -> bool
 val dest_match   : goal sigma -> constr -> marked_term -> constr list
-*)
+i*)
 val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
 val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
-- 
cgit v1.2.3