From cce1b6f06f9802f4d7c977322cec654ad2582d63 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 12 Feb 2015 16:43:28 +0100 Subject: Fix bug #3960: potential evar instance categorized as an unresolvable goal in Instance. Also remove some dead code. --- toplevel/classes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel') diff --git a/toplevel/classes.ml b/toplevel/classes.ml index f44ac36788..01b560d0c4 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -165,7 +165,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in let env' = push_rel_context ctx env in evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars; + evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars; let subst = List.map (Evarutil.nf_evar !evars) subst in if abstract then begin @@ -232,7 +232,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, Misctypes.IntroAnonymous, None) :: props), rest + (CHole (Loc.ghost, None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None) :: props), rest else props, rest) ([], props) k.cl_props in -- cgit v1.2.3 From a91df5fdc60977accd7937eb17b62bd551d3213a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 17 Feb 2015 22:41:26 +0100 Subject: Remove Whelp commands. Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive. --- toplevel/toplevel.mllib | 1 - toplevel/whelp.ml4 | 224 ------------------------------------------------ toplevel/whelp.mli | 20 ----- 3 files changed, 245 deletions(-) delete mode 100644 toplevel/whelp.ml4 delete mode 100644 toplevel/whelp.mli (limited to 'toplevel') diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d22524e5ca..bf0f305abd 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -13,7 +13,6 @@ Record Vernacinterp Mltop Vernacentries -Whelp Vernac Usage Coqloop diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 deleted file mode 100644 index daedc30f42..0000000000 --- a/toplevel/whelp.ml4 +++ /dev/null @@ -1,224 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* !whelp_server_name); - optwrite = (fun s -> whelp_server_name := s) } - -let _ = - declare_string_option - { optsync = false; - optdepr = false; - optname = "Whelp getter"; - optkey = ["Whelp";"Getter"]; - optread = (fun () -> !getter_server_name); - optwrite = (fun s -> getter_server_name := s) } - - -let make_whelp_request req c = - !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req - -let b = Buffer.create 16 - -let url_char c = - if 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' || - '0' <= c && c <= '9' || c ='.' - then Buffer.add_char b c - else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c)) - -let url_string s = String.iter url_char s - -let rec url_list_with_sep sep f = function - | [] -> () - | [a] -> f a - | a::l -> f a; url_string sep; url_list_with_sep sep f l - -let url_id id = url_string (Id.to_string id) - -let uri_of_dirpath dir = - url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir) - -let error_whelp_unknown_reference ref = - let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in - errorlabstrm "" - (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++ - strbrk ", are not supported in Whelp.") - -let uri_of_repr_kn ref (mp,dir,l) = - match mp with - | MPfile sl -> - uri_of_dirpath (Label.to_id l :: DirPath.repr dir @ DirPath.repr sl) - | _ -> - error_whelp_unknown_reference ref - -let url_paren f l = url_char '('; f l; url_char ')' -let url_bracket f l = url_char '['; f l; url_char ']' - -let whelp_of_glob_sort = function - | GProp -> "Prop" - | GSet -> "Set" - | GType _ -> "Type" - -let uri_int n = Buffer.add_string b (string_of_int n) - -let uri_of_ind_pointer l = - url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l - -let uri_of_global ref = - match ref with - | VarRef id -> error ("Unknown Whelp reference: "^(Id.to_string id)^".") - | ConstRef cst -> - uri_of_repr_kn ref (repr_con cst); url_string ".con" - | IndRef (kn,i) -> - uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1] - | ConstructRef ((kn,i),j) -> - uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j] - -let whelm_special = Id.of_string "WHELM_ANON_VAR" - -let url_of_name = function - | Name id -> url_id id - | Anonymous -> url_id whelm_special (* No anon id in Whelp *) - -let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c - -let uri_params f = function - | [] -> () - | l -> url_string "\\subst"; - url_bracket (url_list_with_sep ";" (uri_of_binding f)) l - -let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) - -let section_parameters = function - | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) -> - get_discharged_hyp_names (path_of_global (IndRef(induri,0))) - | GRef (_,(ConstRef cst as ref),_) -> - get_discharged_hyp_names (path_of_global ref) - | _ -> [] - -let merge vl al = - let rec aux acc = function - | ([],l) | (_,([] as l)) -> List.rev acc, l - | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al) - in aux [] (vl,al) - -let rec uri_of_constr c = - match c with - | GVar (_,id) -> url_id id - | GRef (_,ref,_) -> uri_of_global ref - | GHole _ | GEvar _ -> url_string "?" - | GSort (_,s) -> url_string (whelp_of_glob_sort s) - | GApp (_,f,args) -> - let inst,rest = merge (section_parameters f) args in - uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; - url_list_with_sep " " uri_of_constr rest - | GLambda (_,na,k,ty,c) -> - url_string "\\lambda "; url_of_name na; url_string ":"; - uri_of_constr ty; url_string "."; uri_of_constr c - | GProd (_,Anonymous,k,ty,c) -> - uri_of_constr ty; url_string "\\to "; uri_of_constr c - | GProd (_,Name id,k,ty,c) -> - url_string "\\forall "; url_id id; url_string ":"; - uri_of_constr ty; url_string "."; uri_of_constr c - | GLetIn (_,na,b,c) -> - url_string "let "; url_of_name na; url_string "\\def "; - uri_of_constr b; url_string " in "; uri_of_constr c - | GCast (_,c, (CastConv t|CastVM t|CastNative t)) -> - uri_of_constr c; url_string ":"; uri_of_constr t - | GRec _ | GIf _ | GLetTuple _ | GCases _ -> - error "Whelp does not support pattern-matching and (co-)fixpoint." - | GCast (_,_, CastCoerce) -> - anomaly (Pp.str "Written w/o parenthesis") - | GPatVar _ -> - anomaly (Pp.str "Found constructors not supported in constr") - -let make_string f x = Buffer.reset b; f x; Buffer.contents b - -let send_whelp req s = - let url = make_whelp_request req s in - let command = Util.subst_command_placeholder browser_cmd_fmt url in - let _ = CUnix.run_command ~hook:print_string command in () - -let whelp_constr env sigma req c = - let c = detype false [whelm_special] env sigma c in - send_whelp req (make_string uri_of_constr c) - -let whelp_constr_expr req c = - let (sigma,env)= Lemmas.get_current_context () in - let _,c = interp_open_constr env sigma c in - whelp_constr env sigma req c - -let whelp_locate s = - send_whelp "locate" s - -let whelp_elim ind = - send_whelp "elim" (make_string uri_of_global (IndRef ind)) - -let on_goal f = - let gls = Proof.V82.subgoals (get_pftreestate ()) in - let gls = { gls with Evd.it = List.hd gls.Evd.it } in - f (pf_env gls) (project gls) (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) - -type whelp_request = - | Locate of string - | Elim of inductive - | Constr of string * constr - -let whelp = function - | Locate s -> whelp_locate s - | Elim ind -> whelp_elim ind - | Constr (s,c) -> whelp_constr (Global.env()) (Evd.empty) s c - -VERNAC ARGUMENT EXTEND whelp_constr_request -| [ "Match" ] -> [ "match" ] -| [ "Instance" ] -> [ "instance" ] -END - -VERNAC COMMAND EXTEND Whelp CLASSIFIED AS QUERY -| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ] -| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] -END - -VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY -| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] -| [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] -> - [ on_goal (fun env sigma -> whelp_constr env sigma "hint") ] -END diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli deleted file mode 100644 index 62272c50ff..0000000000 --- a/toplevel/whelp.mli +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit -- cgit v1.2.3 From cdbfad340dcd8cd3428853886964882b389776c6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 18 Feb 2015 12:04:30 +0100 Subject: Fix bug #4046. --- toplevel/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 01b560d0c4..07f881721d 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro let get_id = function | Ident id' -> id' - | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") + | Qualid (loc,id') -> (loc, snd (repr_qualid id')) in let props, rest = List.fold_left -- cgit v1.2.3