diff options
| author | filliatr | 2000-05-03 20:44:42 +0000 |
|---|---|---|
| committer | filliatr | 2000-05-03 20:44:42 +0000 |
| commit | bae7532aaf4fc4ca0f637cb6e53f6b4b80c7cb75 (patch) | |
| tree | e4c5a1725f1d12b78b959e974f61380f55557806 /tactics | |
| parent | 5c64bc0eb899409b66b3e13fe99ebf679b0850a7 (diff) | |
diverses modifs pour ocamlweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hipattern.mli | 7 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 4 |
2 files changed, 6 insertions, 5 deletions
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 |