From fd8b1d101c07c69252719e9e35209baf019216be Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:41:00 +0000
Subject: Scope type pour le codomaine de Prod aussi; ajout extern_rawtype

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

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7b07e0a96b..d940aae37f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -20,7 +20,6 @@ open Inductive
 open Sign
 open Environ
 open Libnames
-open Declare
 open Impargs
 open Topconstr
 open Rawterm
@@ -573,7 +572,7 @@ and factorize_prod scopes vars aty = function
 	-> let id = avoid_wildcard id in
            let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
            ((loc,Name id)::nal,c)
-  | c -> ([],extern true scopes vars c)
+  | c -> ([],extern_type scopes vars c)
 
 and factorize_lambda inctx scopes vars aty = function
   | RLambda (loc,na,ty,c)
@@ -637,6 +636,9 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 let extern_rawconstr vars c = 
   extern false (None,Symbols.current_scopes()) vars c
 
+let extern_rawtype vars c =
+  extern_type (None,Symbols.current_scopes()) vars c
+
 let extern_cases_pattern vars p = 
   extern_cases_pattern_in_scope (Symbols.current_scopes()) vars p
 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index c5595f5a9e..d088867c54 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -33,6 +33,7 @@ val check_same_type : constr_expr -> constr_expr -> unit
 
 val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
 val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
+val extern_rawtype : Idset.t -> rawconstr -> constr_expr
 val extern_pattern : env -> names_context -> constr_pattern -> constr_expr
 
 (* If [b=true] in [extern_constr b env c] then the variables in the first 
-- 
cgit v1.2.3