From 9c46109dcf1649080bb13bab4bf02f6d3a34045c Mon Sep 17 00:00:00 2001
From: bgregoir
Date: Fri, 27 Oct 2006 13:29:22 +0000
Subject: changement des _sym par _comm dans setoid_ring

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

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 516caf3ed5..aeb4d294bc 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -93,3 +93,8 @@ val type_fixpoint : env -> name array -> types array
 (* Kernel safe typing but applicable to partial proofs *)
 val typing : env -> constr -> unsafe_judgment
 
+(* A virer *)
+val execute : Environ.env ->
+    Term.types ->
+    Univ.Constraint.t * Univ.universes ->
+    Environ.unsafe_judgment * (Univ.Constraint.t * Univ.universes)
-- 
cgit v1.2.3