diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 10 | ||||
| -rw-r--r-- | interp/notation.ml | 26 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 | ||||
| -rw-r--r-- | interp/topconstr.ml | 8 |
4 files changed, 31 insertions, 15 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index b44cabe8b8..90432a4a47 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -66,14 +66,20 @@ let gen_constant_in_modules locstr dirs s = let check_required_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in + let mp = (fst(Lib.current_prefix())) in + let current_dir = match mp with + | MPfile dp -> (dir=dp) + | _ -> false + in if not (Library.library_is_loaded dir) then + if not current_dir then (* Loading silently ... let m, prefix = list_sep_last d' in read_library (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) *) (* or failing ...*) - error ("Library "^(string_of_dirpath dir)^" has to be required first.") + error ("Library "^(string_of_dirpath dir)^" has to be required first.") (************************************************************************) (* Specific Coq objects *) @@ -123,7 +129,7 @@ let jmeq_module_name = ["Coq";"Logic";"JMeq"] let jmeq_module = make_dir jmeq_module_name (* TODO: temporary hack *) -let make_kn dir id = Libnames.encode_kn dir id +let make_kn dir id = Libnames.encode_mind dir id let make_con dir id = Libnames.encode_con dir id (** Identity *) diff --git a/interp/notation.ml b/interp/notation.ml index 342cb6c9cf..8f9f0959d5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -109,7 +109,7 @@ let open_scope i (_,(local,op,sc)) = let cache_scope o = open_scope 1 o -let subst_scope (_,subst,sc) = sc +let subst_scope (subst,sc) = sc open Libobject @@ -180,19 +180,29 @@ type key = let notations_key_table = ref Gmapl.empty let prim_token_key_table = Hashtbl.create 7 + +let make_gr = function + | ConstRef con -> + ConstRef(constant_of_kn(canonical_con con)) + | IndRef (kn,i) -> + IndRef(mind_of_kn(canonical_mind kn),i) + | ConstructRef ((kn,i),j )-> + ConstructRef((mind_of_kn(canonical_mind kn),i),j) + | VarRef id -> VarRef id + let rawconstr_key = function - | RApp (_,RRef (_,ref),_) -> RefKey ref - | RRef (_,ref) -> RefKey ref + | RApp (_,RRef (_,ref),_) -> RefKey (make_gr ref) + | RRef (_,ref) -> RefKey (make_gr ref) | _ -> Oth let cases_pattern_key = function - | PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref) + | PatCstr (_,ref,_,_) -> RefKey (make_gr (ConstructRef ref)) | _ -> Oth let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) - | AApp (ARef ref,args) -> RefKey ref, Some (List.length args) - | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args) - | ARef ref -> RefKey ref, None + | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args) + | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey (make_gr ref), Some (List.length args) + | ARef ref -> RefKey(make_gr ref), None | _ -> Oth, None (**********************************************************************) @@ -458,7 +468,7 @@ let load_arguments_scope _ (_,(_,r,scl)) = let cache_arguments_scope o = load_arguments_scope 1 o -let subst_arguments_scope (_,subst,(req,r,scl)) = +let subst_arguments_scope (subst,(req,r,scl)) = (ArgsScopeNoDischarge,fst (subst_global subst r),scl) let discharge_arguments_scope (_,(req,r,l)) = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 939fe01aa4..1330a3689b 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -51,7 +51,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let cache_syntax_constant d = load_syntax_constant 1 d -let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) = +let subst_syntax_constant (subst,(local,pat,onlyparse)) = (local,subst_interpretation subst pat,onlyparse) let classify_syntax_constant (local,_,_ as o) = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index bea0eae314..ec1b20a12b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -143,7 +143,7 @@ let has_ldots = (function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false) let compare_rawconstr f t1 t2 = match t1,t2 with - | RRef (_,r1), RRef (_,r2) -> r1 = r2 + | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2 | RVar (_,v1), RVar (_,v2) -> v1 = v2 | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2 | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> @@ -281,7 +281,7 @@ let rec subst_pat subst pat = match pat with | PatVar _ -> pat | PatCstr (loc,((kn,i),j),cpl,n) -> - let kn' = subst_kn subst kn + let kn' = subst_ind subst kn and cpl' = list_smartmap (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (loc,((kn',i),j),cpl',n) @@ -331,7 +331,7 @@ let rec subst_aconstr subst bound raw = (fun (a,(n,signopt) as x) -> let a' = subst_aconstr subst bound a in let signopt' = Option.map (fun ((indkn,i),n,nal as z) -> - let indkn' = subst_kn subst indkn in + let indkn' = subst_ind subst indkn in if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl @@ -485,7 +485,7 @@ let adjust_application_n n loc f l = let rec match_ alp metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1 | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma - | RRef (_,r1), ARef r2 when r1 = r2 -> sigma + | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma | RApp (loc,f1,l1), AApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in |