instanciation des opérateurs sur la bonne signature (celle de

définition, puisqu'elle ne peut pas changer, mais qu'elle peut être un
préfixe)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@45 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 2 deletions

diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 6eb89dab6..7255eb721 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -6,11 +6,14 @@ open Util
 open Names
 open Generic
 open Term
+open Sign
 open Constant
 open Inductive
 open Typing
 open G_minicoq
 
+let (env : unit environment ref) = ref empty_environment
+
 let lookup_var id =
   let rec look n = function
     | [] -> VAR id
@@ -19,18 +22,24 @@ let lookup_var id =
   in
   look 1
 
+let args sign = Array.of_list (List.map (fun id -> VAR id) (fst sign))
+
 let rec globalize bv = function
   | VAR id -> lookup_var id bv
   | DOP1 (op,c) -> DOP1 (op, globalize bv c)
   | DOP2 (op,c1,c2) -> DOP2 (op, globalize bv c1, globalize bv c2)
+  | DOPN (Const sp as op, _) ->
+      let cb = lookup_constant sp !env in DOPN (op, args cb.const_hyps)
+  | DOPN (MutInd (sp,_) as op, _) ->
+      let mib = lookup_mind sp !env in DOPN (op, args mib.mind_hyps)
+  | DOPN (MutConstruct ((sp,_),_) as op, _) ->
+      let mib = lookup_mind sp !env in DOPN (op, args mib.mind_hyps)
   | DOPN (op,v) -> DOPN (op, Array.map (globalize bv) v)
   | DOPL (op,l) -> DOPL (op, List.map (globalize bv) l)
   | DLAM (na,c) -> DLAM (na, globalize (na::bv) c)
   | DLAMV (na,v) -> DLAMV (na, Array.map (globalize (na::bv)) v)
   | Rel _ | DOP0 _ as c -> c
 
-let (env : unit environment ref) = ref empty_environment
-
 let check c = 
   let c = globalize [] c in
   let (j,u) = safe_machine !env c in