From bea2a4f5fe5cab0abfc27492117c335a311a0c19 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 12 Jun 2013 21:07:40 +0000
Subject: Changing the type of Ltac values. Now they are toplevel generic
 arguments. That way we will be able to define interpretation of tactics
 without referring to tactic values.

Quite ad-hoc for now.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/genarg.ml  | 2 ++
 interp/genarg.mli | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'interp')

diff --git a/interp/genarg.ml b/interp/genarg.ml
index eb5287b323..f9b5bee0a4 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -197,6 +197,8 @@ let app_pair f1 f2 = function
       (u, Obj.repr (o1,o2))
   | _ -> failwith "Genarg: not a pair"
 
+let has_type (t, v) u = argument_type_eq t u
+
 let unquote x = x
 
 type an_arg_of_this_type = Obj.t
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 7f9d39907c..4f5dea7ec0 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -161,6 +161,10 @@ val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a
 (** [out_gen t x] recovers an argument of type [t] from a generic argument. It
     fails if [x] has not the right dynamic type. *)
 
+val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
+(** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
+    [out_gen t v] will not raise a dynamic type exception. *)
+
 (** {6 Manipulation of generic arguments}
 
 Those functions fail if they are applied to an argument which has not the right
-- 
cgit v1.2.3