From 02f6cb08e4b8f892594934766a40413a3fa30342 Mon Sep 17 00:00:00 2001
From: coq
Date: Tue, 1 Oct 2002 07:53:07 +0000
Subject: Vraie substitutivite de autohints

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pattern.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'pretyping/pattern.mli')

diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 5ff667f90b..943a8d8c3d 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -35,6 +35,8 @@ type constr_pattern =
 
 val occur_meta_pattern : constr_pattern -> bool
 
+val subst_pattern : substitution -> constr_pattern -> constr_pattern
+
 type constr_label =
   | ConstNode of constant
   | IndNode of inductive
@@ -43,6 +45,8 @@ type constr_label =
 
 val label_of_ref : global_reference -> constr_label
 
+val subst_label : substitution -> constr_label -> constr_label
+
 exception BoundPattern
 
 (* [head_pattern_bound t] extracts the head variable/constant of the
-- 
cgit v1.2.3