diff options
| author | gmelquio | 2009-11-04 18:47:36 +0000 |
|---|---|---|
| committer | gmelquio | 2009-11-04 18:47:36 +0000 |
| commit | 208eceab14148fa561c36f71e2e1485e73832616 (patch) | |
| tree | 3763b73a349cca213cee543f8cf0204d65594ae6 /toplevel | |
| parent | fc7f18e8596a8b4e690ff726edb02a7cf319edbd (diff) | |
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
Fixed pretty printing of record syntax.
Allowed record syntax inside patterns. (Patch by Cedric Auger.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 7fdd6bd7e4..de2e78ba54 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -200,7 +200,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) | _ -> if List.length k.cl_props <> 1 then errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body") - else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props] + else [Ident (dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props] in let subst = match k.cl_props with @@ -211,12 +211,18 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) let c = interp_casted_constr_evars evars env' term ty' in c :: subst | _ -> + let get_id = + function + | Ident id' -> id' + | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") + in let props, rest = List.fold_left (fun (props, rest) (id,b,_) -> try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in + let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in + let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in + let (loc, mid) = get_id loc_mid in Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); c :: props, rest' with Not_found -> @@ -224,7 +230,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) ([], props) k.cl_props in if rest <> [] then - unbound_method env' k.cl_impl (fst (List.hd rest)) + unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) else type_ctx_instance evars env' k.cl_props props subst in |