From a4f64ba3e82546d2cc57b6c2be4bad0d52364863 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 8 Jan 2006 17:13:38 +0000
Subject: Ajout rawconstr_of_aconstr

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

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ad21e5b371..61e03fb3f7 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -99,6 +99,11 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
   | APatVar n -> RPatVar (loc,(false,n))
   | ARef x -> RRef (loc,x)
 
+let rec rawconstr_of_aconstr loc x =
+  let rec aux () x = 
+    rawconstr_of_aconstr_with_binders loc (fun id () -> (id,())) aux () x
+  in aux () x
+
 let rec subst_pat subst pat = 
   match pat with
   | PatVar _ -> pat
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index c7cc74b0f8..84342b2209 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -47,6 +47,8 @@ val rawconstr_of_aconstr_with_binders : loc ->
   (identifier -> 'a -> identifier * 'a) ->
   ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
 
+val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
+
 val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr
 
 val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
-- 
cgit v1.2.3