diff options
| author | herbelin | 2000-11-06 22:01:12 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-06 22:01:12 +0000 |
| commit | 901f1b200feea81c3c9129b153dce067e41b9770 (patch) | |
| tree | 94a16f7af19608665aad2a52d03b5bed8dd98ad8 /pretyping | |
| parent | fc1c97e844dd2710bbe8c1b7e9244ef05d349d1a (diff) | |
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de DischargeAt)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/class.ml | 8 | ||||
| -rw-r--r-- | pretyping/class.mli | 6 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 3 |
3 files changed, 7 insertions, 10 deletions
diff --git a/pretyping/class.ml b/pretyping/class.ml index 6dfb3ca0b9..75f4ee52d9 100644 --- a/pretyping/class.ml +++ b/pretyping/class.ml @@ -22,7 +22,8 @@ let stre_gt = function | (NeverDischarge,NeverDischarge) -> false | (NeverDischarge,x) -> false | (x,NeverDischarge) -> true - | (DischargeAt sp1,DischargeAt sp2) -> sp_gt (sp1,sp2) + | (DischargeAt sp1,DischargeAt sp2) -> + dirpath_prefix_of sp1 sp2 (* was sp_gt but don't understand why - HH *) let stre_max (stre1,stre2) = if stre_gt (stre1,stre2) then stre1 else stre2 @@ -365,10 +366,7 @@ let try_add_new_coercion_record id stre source = (* fonctions pour le discharge: plutot sale *) -let defined_in_sec sp sec_sp = - let ((p1,id1,k1)) = repr_path sp in - let ((p2,id2,k2)) = repr_path sec_sp in - p1 = (string_of_id id2)::p2 +let defined_in_sec sp sec_sp = dirpath sp = sec_sp let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) = let env = Global.env () in diff --git a/pretyping/class.mli b/pretyping/class.mli index dc19ccce01..e88b3ccf02 100644 --- a/pretyping/class.mli +++ b/pretyping/class.mli @@ -18,9 +18,7 @@ val try_add_new_coercion_with_target : identifier -> strength -> val try_add_new_class : identifier -> strength -> unit val process_class : - section_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) + dir_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) val process_coercion : - section_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> + dir_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int - -val defined_in_sec : section_path -> section_path -> bool diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0807541724..f4cc94fd6a 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -20,13 +20,14 @@ let rec filter_unique = function if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l) else x::filter_unique l +(* let distinct_id_list = let rec drec fresh = function [] -> List.rev fresh | id::rest -> let id' = next_ident_away_from id fresh in drec (id'::fresh) rest in drec [] - +*) (* let filter_sign p sign x = |