diff options
38 files changed, 264 insertions, 192 deletions
diff --git a/.gitignore b/.gitignore index 63da6b4d0e..538124b8e5 100644 --- a/.gitignore +++ b/.gitignore @@ -68,6 +68,7 @@ time-of-build-after.log .csdp.cache test-suite/.lia.cache test-suite/.nra.cache +test-suite/.nia.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt @@ -135,7 +136,6 @@ coqpp/coqpp_parse.mli g_*.ml lib/coqProject_file.ml -parsing/cLexer.ml plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml plugins/ltac/extraargs.ml @@ -166,8 +166,6 @@ checker/esubst.mli user-contrib .*.sw* .#* -test-suite/.lia.cache -test-suite/.nra.cache plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml diff --git a/Makefile.build b/Makefile.build index 4d19f9a2e1..77fcfc0abf 100644 --- a/Makefile.build +++ b/Makefile.build @@ -406,7 +406,7 @@ grammar/%.cmi: grammar/%.mli .PHONY: coqbinaries coqbyte -coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) $(GRAMMARCMA) coqbyte: $(TOPBYTE) $(CHICKENBYTE) # Special rule for coqtop, we imitate `ocamlopt` can delete the target diff --git a/engine/namegen.ml b/engine/namegen.ml index 7ce759a3fb..db72dc8ec3 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,7 +21,6 @@ open Constr open Environ open EConstr open Vars -open Nametab open Nameops open Libnames open Globnames @@ -82,14 +81,14 @@ let is_imported_ref = function let is_global id = try - let ref = locate (qualid_of_ident id) in + let ref = Nametab.locate (qualid_of_ident id) in not (is_imported_ref ref) with Not_found -> false let is_constructor id = try - match locate (qualid_of_ident id) with + match Nametab.locate (qualid_of_ident id) with | ConstructRef _ -> true | _ -> false with Not_found -> @@ -116,7 +115,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) | Cast (c,_,_) | App (c,_) -> hdrec c | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn))) | Const _ | Ind _ | Construct _ | Var _ as c -> - Some (basename_of_global (global_of_constr c)) + Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None @@ -148,8 +147,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) - | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") - | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> @@ -267,7 +266,7 @@ let visible_ids sigma (nenv, c) = begin try let gseen = GlobRef.Set_env.add g gseen in - let short = shortest_qualid_of_global Id.Set.empty g in + let short = Nametab.shortest_qualid_of_global Id.Set.empty g in let dir, id = repr_qualid short in let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in accu := (gseen, vseen, ids) diff --git a/engine/univGen.ml b/engine/univGen.ml index 23ab30eb75..130aa06f53 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -77,17 +77,14 @@ let fresh_global_instance ?loc ?names env gr = let u, ctx = fresh_global_instance ?loc ?names env gr in mkRef (gr, u), ctx -let constr_of_global gr = - let c, ctx = fresh_global_instance (Global.env ()) gr in - if not (Univ.ContextSet.is_empty ctx) then - if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then - (* Should be an error as we might forget constraints, allow for now - to make firstorder work with "using" clauses *) - c - else CErrors.user_err ~hdr:"constr_of_global" - Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ - str " would forget universes.") - else c +let constr_of_monomorphic_global gr = + if not (Global.is_polymorphic gr) then + fst (fresh_global_instance (Global.env ()) gr) + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") + +let constr_of_global gr = constr_of_monomorphic_global gr let constr_of_global_univ = mkRef diff --git a/engine/univGen.mli b/engine/univGen.mli index c2e9d0c696..42756701dc 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -74,11 +74,16 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> [@@ocaml.deprecated "Use [Univ.extend_in_context_set]"] (** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) + the proper way to get a fresh copy of a polymorphic global reference. *) +val constr_of_monomorphic_global : GlobRef.t -> constr + val constr_of_global : GlobRef.t -> constr +[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\ + use [constr_of_monomorphic_global] if the reference is guaranteed to\ + be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"] (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 98e1f6dd36..601099c6ff 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,7 +26,6 @@ open Notation_ops open Glob_term open Glob_ops open Pattern -open Nametab open Notation open Detyping open Decl_kinds @@ -213,7 +212,7 @@ let is_record indsp = with Not_found -> false let encode_record r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in if not (is_record indsp) then user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); @@ -279,7 +278,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - shortest_qualid_of_global ?loc vars r + Nametab.shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -481,7 +480,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> - let qid = shortest_qualid_of_syndef ?loc vars kn in + let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) @@ -1136,7 +1135,7 @@ and extern_notation (custom,scopes as allscopes) vars t = function List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in - let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in + let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d7497d4e8e..6b22261a15 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -28,7 +28,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Nametab open Notation open Inductiveops open Decl_kinds @@ -633,7 +632,7 @@ let terms_of_binders bl = | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in + let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in @@ -721,7 +720,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = try let gc = intern nenv c in Id.Map.add id (gc, Some c) map - with GlobalizationError _ -> map + with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -986,7 +985,7 @@ let intern_extended_global_of_qualid qid = let intern_reference qid = let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in Smartlocate.global_of_extended_global r @@ -1058,11 +1057,11 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qi (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,qualid_basename qid) us, [], [], []), args - else error_global_not_found qid + else Nametab.error_global_not_found qid else let r,projapp,args2 = try intern_qualid qid intern env ntnvars us args - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 @@ -1312,7 +1311,7 @@ let sort_fields ~complete loc fields completer = (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try shortest_qualid_of_global ?loc Id.Set.empty global_record_id + try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1493,7 +1492,7 @@ let drop_notations_pattern looked_for genv = in let rec drop_syndef top scopes qid pats = try - match locate_extended qid with + match Nametab.locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1550,7 +1549,7 @@ let drop_notations_pattern looked_for genv = | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (qid, Some expl_pl, pl) -> - let g = try locate qid + let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index e3d490a1ad..b73d238c22 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -15,7 +15,6 @@ open Names open Libnames open Libobject open Lib -open Nametab open Notation_term (* Syntactic definitions. *) @@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let is_alias_of_already_visible_name sp = function | _,NRef ref -> - let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in + let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in DirPath.is_empty dir && Id.equal id (basename sp) | _ -> false @@ -83,11 +82,11 @@ let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) let pr_compat_warning (kn, def, v) = let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r + | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r | _ -> strbrk " is a compatibility notation" in pr_syndef kn ++ pp_def diff --git a/library/coqlib.ml b/library/coqlib.ml index 677515981a..a044a9a395 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -14,7 +14,6 @@ open Pp open Names open Libnames open Globnames -open Nametab let make_dir l = DirPath.make (List.rev_map Id.of_string l) @@ -79,7 +78,7 @@ let register_ref s c = (* Generic functions to find Coq objects *) let has_suffix_in_dirs dirs ref = - let dir = dirpath (path_of_global ref) in + let dir = dirpath (Nametab.path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs let gen_reference_in_modules locstr dirs s = diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml index 9c421f5b76..2230dfc47c 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml @@ -229,9 +229,11 @@ let unlocated f x = f x (* try f x with Loc.Exc_located (_, exc) -> raise exc *) let check_keyword str = - let rec loop_symb = parser - | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str - | [< s >] -> + let rec loop_symb s = match Stream.peek s with + | Some (' ' | '\n' | '\r' | '\t' | '"') -> + Stream.junk s; + bad_token str + | _ -> match unlocated lookup_utf8 Ploc.dummy s with | Utf8Token (_,n) -> njunk n s; loop_symb s | AsciiChar -> Stream.junk s; loop_symb s @@ -240,12 +242,14 @@ let check_keyword str = loop_symb (Stream.of_string str) let check_ident str = - let rec loop_id intail = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] -> + let rec loop_id intail s = match Stream.peek s with + | Some ('a'..'z' | 'A'..'Z' | '_') -> + Stream.junk s; loop_id true s - | [< ' ('0'..'9' | ''') when intail; s >] -> + | Some ('0'..'9' | '\'') when intail -> + Stream.junk s; loop_id true s - | [< s >] -> + | _ -> match unlocated lookup_utf8 Ploc.dummy s with | Utf8Token (st, n) when not intail && Unicode.is_valid_ident_initial st -> njunk n s; loop_id true s | Utf8Token (st, n) when intail && Unicode.is_valid_ident_trailing st -> @@ -308,10 +312,11 @@ let warn_unrecognized_unicode = strbrk (Printf.sprintf "Not considering unicode character \"%s\" of unknown \ lexical status as part of identifier \"%s\"." u id)) -let rec ident_tail loc len = parser - | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> +let rec ident_tail loc len s = match Stream.peek s with + | Some ('a'..'z' | 'A'..'Z' | '0'..'9' | '\'' | '_' as c) -> + Stream.junk s; ident_tail loc (store len c) s - | [< s >] -> + | _ -> match lookup_utf8 loc s with | Utf8Token (st, n) when Unicode.is_valid_ident_trailing st -> ident_tail loc (nstore n len s) s @@ -321,9 +326,9 @@ let rec ident_tail loc len = parser warn_unrecognized_unicode ~loc:!@loc (u,id); len | _ -> len -let rec number len = parser - | [< ' ('0'..'9' as c); s >] -> number (store len c) s - | [< >] -> len +let rec number len s = match Stream.peek s with + | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s + | _ -> len let warn_comment_terminator_in_string = CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing" @@ -335,31 +340,43 @@ let warn_comment_terminator_in_string = (* If the string being lexed is in a comment, [comm_level] is Some i with i the current level of comments nesting. Otherwise, [comm_level] is None. *) -let rec string loc ~comm_level bp len = parser - | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> +let rec string loc ~comm_level bp len s = match Stream.peek s with + | Some '"' -> + Stream.junk s; + let esc = + match Stream.peek s with + Some '"' -> Stream.junk s; true + | _ -> false + in if esc then string loc ~comm_level bp (store len '"') s else (loc, len) - | [< ''('; s >] -> - (parser - | [< ''*'; s >] -> + | Some '(' -> + Stream.junk s; + (fun s -> match Stream.peek s with + | Some '*' -> + Stream.junk s; let comm_level = Option.map succ comm_level in string loc ~comm_level bp (store (store len '(') '*') s - | [< >] -> + | _ -> string loc ~comm_level bp (store len '(') s) s - | [< ''*'; s >] -> - (parser - | [< '')'; s >] -> + | Some '*' -> + Stream.junk s; + (fun s -> match Stream.peek s with + | Some ')' -> + Stream.junk s; let () = match comm_level with | Some 0 -> - warn_comment_terminator_in_string ~loc:!@loc () + warn_comment_terminator_in_string ~loc:!@loc () | _ -> () in let comm_level = Option.map pred comm_level in string loc ~comm_level bp (store (store len '*') ')') s - | [< >] -> + | _ -> string loc ~comm_level bp (store len '*') s) s - | [< ''\n' as c; s >] ep -> + | Some ('\n' as c) -> + Stream.junk s; + let ep = Stream.count s in (* If we are parsing a comment, the string if not part of a token so we update the first line of the location. Otherwise, we update the last line. *) @@ -368,8 +385,12 @@ let rec string loc ~comm_level bp len = parser else bump_loc_line_last loc ep in string loc ~comm_level bp (store len c) s - | [< 'c; s >] -> string loc ~comm_level bp (store len c) s - | [< _ = Stream.empty >] ep -> + | Some c -> + Stream.junk s; + string loc ~comm_level bp (store len c) s + | _ -> + let _ = Stream.empty s in + let ep = Stream.count s in let loc = set_loc_pos loc bp ep in err loc Unterminated_string @@ -441,25 +462,50 @@ let comment_stop ep = comment_begin := None; between_commands := false -let rec comment loc bp = parser bp2 - | [< ''('; - loc = (parser - | [< ''*'; s >] -> push_string "(*"; comment loc bp s - | [< >] -> push_string "("; loc ); - s >] -> comment loc bp s - | [< ''*'; - loc = parser - | [< '')' >] -> push_string "*)"; loc - | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc - | [< ''"'; s >] -> +let rec comment loc bp s = + let bp2 = Stream.count s in + match Stream.peek s with + Some '(' -> + Stream.junk s; + let loc = + try + match Stream.peek s with + Some '*' -> + Stream.junk s; + push_string "(*"; comment loc bp s + | _ -> push_string "("; loc + with Stream.Failure -> raise (Stream.Error "") + in + comment loc bp s + | Some '*' -> + Stream.junk s; + begin try + match Stream.peek s with + Some ')' -> Stream.junk s; push_string "*)"; loc + | _ -> real_push_char '*'; comment loc bp s + with Stream.Failure -> raise (Stream.Error "") + end + | Some '"' -> + Stream.junk s; let loc, len = string loc ~comm_level:(Some 0) bp2 0 s in push_string "\""; push_string (get_buff len); push_string "\""; comment loc bp s - | [< _ = Stream.empty >] ep -> + | _ -> + match try Some (Stream.empty s) with Stream.Failure -> None with + | Some _ -> + let ep = Stream.count s in let loc = set_loc_pos loc bp ep in err loc Unterminated_comment - | [< ''\n' as z; s >] ep -> real_push_char z; comment (bump_loc_line loc ep) bp s - | [< 'z; s >] -> real_push_char z; comment loc bp s + | _ -> + match Stream.peek s with + Some ('\n' as z) -> + Stream.junk s; + let ep = Stream.count s in + real_push_char z; comment (bump_loc_line loc ep) bp s + | Some z -> + Stream.junk s; + real_push_char z; comment loc bp s + | _ -> raise Stream.Failure (* Parse a special token, using the [token_tree] *) @@ -526,12 +572,16 @@ let process_chars loc bp c cs = (* Parse what follows a dot *) -let parse_after_dot loc c bp = - parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d); s >] -> +let parse_after_dot loc c bp s = match Stream.peek s with + | Some ('a'..'z' | 'A'..'Z' | '_' as d) -> + Stream.junk s; + let len = + try ident_tail loc (store 0 d) s with + Stream.Failure -> raise (Stream.Error "") + in let field = get_buff len in (try find_keyword loc ("."^field) s with Not_found -> FIELD field) - | [< s >] -> + | _ -> match lookup_utf8 loc s with | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in @@ -559,12 +609,23 @@ let blank_or_eof cs = (* Parse a token in a char stream *) -let rec next_token loc = parser bp - | [< ''\n' as c; s >] ep -> +let rec next_token loc s = + let bp = Stream.count s in + match Stream.peek s with + | Some ('\n' as c) -> + Stream.junk s; + let ep = Stream.count s in comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s - | [< '' ' | '\t' | '\r' as c; s >] -> + | Some (' ' | '\t' | '\r' as c) -> + Stream.junk s; comm_loc bp; push_char c; next_token loc s - | [< ''.' as c; t = parse_after_dot loc c bp; s >] ep -> + | Some ('.' as c) -> + Stream.junk s; + let t = + try parse_after_dot loc c bp s with + Stream.Failure -> raise (Stream.Error "") + in + let ep = Stream.count s in comment_stop bp; (* We enforce that "." should either be part of a larger keyword, for instance ".(", or followed by a blank or eof. *) @@ -575,42 +636,68 @@ let rec next_token loc = parser bp between_commands := true; | _ -> () in - (t, set_loc_pos loc bp ep) - | [< ' ('-'|'+'|'*' as c); s >] -> + t, set_loc_pos loc bp ep + | Some ('-' | '+' | '*' as c) -> + Stream.junk s; let t,new_between_commands = if !between_commands then process_sequence loc bp c s, true else process_chars loc bp c s,false in comment_stop bp; between_commands := new_between_commands; t - | [< ''?'; s >] ep -> + | Some '?' -> + Stream.junk s; + let ep = Stream.count s in let t = parse_after_qmark loc bp s in comment_stop bp; (t, set_loc_pos loc bp ep) - | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail loc (store 0 c); s >] ep -> + | Some ('a'..'z' | 'A'..'Z' | '_' as c) -> + Stream.junk s; + let len = + try ident_tail loc (store 0 c) s with + Stream.Failure -> raise (Stream.Error "") + in + let ep = Stream.count s in let id = get_buff len in comment_stop bp; (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep - | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> + | Some ('0'..'9' as c) -> + Stream.junk s; + let len = + try number (store 0 c) s with + Stream.Failure -> raise (Stream.Error "") + in + let ep = Stream.count s in comment_stop bp; (INT (get_buff len), set_loc_pos loc bp ep) - | [< ''\"'; (loc,len) = string loc ~comm_level:None bp 0 >] ep -> + | Some '\"' -> + Stream.junk s; + let (loc, len) = + try string loc ~comm_level:None bp 0 s with + Stream.Failure -> raise (Stream.Error "") + in + let ep = Stream.count s in comment_stop bp; (STRING (get_buff len), set_loc_pos loc bp ep) - | [< ' ('(' as c); - t = parser - | [< ''*'; s >] -> + | Some ('(' as c) -> + Stream.junk s; + begin try + match Stream.peek s with + | Some '*' -> + Stream.junk s; comm_loc bp; push_string "(*"; let loc = comment loc bp s in next_token loc s - | [< t = process_chars loc bp c >] -> comment_stop bp; t >] -> - t - | [< ' ('{' | '}' as c); s >] ep -> + | _ -> let t = process_chars loc bp c s in comment_stop bp; t + with Stream.Failure -> raise (Stream.Error "") + end + | Some ('{' | '}' as c) -> + Stream.junk s; + let ep = Stream.count s in let t,new_between_commands = if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true else process_chars loc bp c s, false in comment_stop bp; between_commands := new_between_commands; t - | [< s >] -> + | _ -> match lookup_utf8 loc s with | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index b9ad1ff6d8..07f50f6cd5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -10,7 +10,7 @@ open Constr -let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n) +let bt_lib_constr n = lazy (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref n) let decomp_term sigma (c : Constr.t) = Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 8fa676de44..b0c4785d7a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -233,12 +233,11 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) -let constant str = UnivGen.constr_of_global - @@ Coqlib.lib_ref str +let constant str = Coqlib.lib_ref str let defined_connectives = lazy - [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); - AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))] + [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type")); + AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 98d68d3db7..ad1114b733 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in - let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in - let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in + let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in + let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in + let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -1605,7 +1605,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 03a64988e4..a385a61ae0 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -116,7 +116,7 @@ let def_of_const t = [@@@ocaml.warning "-3"] let coq_constant s = - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -441,7 +441,7 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) @@ -449,7 +449,7 @@ let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) @@ -463,7 +463,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") [@@@ocaml.warning "-3"] -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" [@@@ocaml.warning "+3"] diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b8973a18dc..b0842c3721 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -511,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca3160f4c4..f9df3aed45 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -51,7 +51,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) [@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "RecursiveDefinition" m s let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] @@ -63,7 +63,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) [@@@ocaml.warning "+3"] @@ -97,7 +97,7 @@ let type_of_const sigma t = Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false -let constant sl s = constr_of_global (find_reference sl s) +let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s) let const_of_ref = function ConstRef kn -> kn @@ -1241,7 +1241,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in + let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 1f2c722b34..a88285c9ee 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -115,7 +115,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = (* Summary and Object declaration *) -open Nametab open Libobject type ltac_entry = { @@ -153,19 +152,19 @@ let tac_deprecation kn = let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Nametab.Until i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Nametab.Exactly i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with | None -> - let () = push_tactic (Until 1) sp kn in + let () = push_tactic (Nametab.Until 1) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 5501cf92a5..55412c74bb 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -19,7 +19,6 @@ open Util open Names open Libnames open Globnames -open Nametab open Smartlocate open Constrexpr open Termops @@ -98,7 +97,7 @@ let intern_global_reference ist qid = ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) else try ArgArg (qid.CAst.loc,locate_global_with_alias qid) - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -150,7 +149,7 @@ let intern_isolated_tactic_reference strict ist qid = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Internalize an applied tactic reference *) @@ -169,7 +168,7 @@ let intern_applied_tactic_reference ist qid = try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) @@ -190,7 +189,7 @@ let intern_non_tactic_reference strict ist qid = TacGeneric ipat else (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -302,7 +301,7 @@ let intern_evaluable_global_reference ist qid = try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) - else error_global_not_found qid + else Nametab.error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -377,7 +376,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f90e889678..b60b77595b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -23,7 +23,6 @@ open Names open Nameops open Libnames open Globnames -open Nametab open Refiner open Tacmach.New open Tactic_debug @@ -358,7 +357,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (qualid_of_ident ?loc id) + | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (qualid_of_ident ?loc id)) + Nametab.error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 11d0a4a44d..ef60a23e80 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -135,7 +135,7 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let tpexpr = gen_constant "plugins.setoid_ring.pexpr" let ttconst = gen_constant "plugins.setoid_ring.const" @@ -540,7 +540,7 @@ let nsatz lpol = let return_term t = let a = - mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in + mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 09bd4cd352..d8adb17710 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -186,7 +186,8 @@ let reset_all () = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr) +let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global + |> EConstr.of_constr) (* Zarith *) diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 79418da27c..840a05e02b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -26,11 +26,11 @@ let step_count = ref 0 let node_count = ref 0 -let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -let li_and = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type")) -let li_or = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type")) +let li_False = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) +let li_and = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type")) +let li_or = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.or.type")) -let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) +let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) let l_xI = gen_constant "num.pos.xI" let l_xO = gen_constant "num.pos.xO" diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9585826109..8dbef47fe1 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -206,7 +206,7 @@ let exec_tactic env evd n f args = let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd -let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n))) +let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))) let gen_reference n = lazy (Coqlib.lib_ref n) let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory" @@ -251,7 +251,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) [@@ocaml.warning "-3"] let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -901,7 +901,7 @@ let ftheory_to_obj : field_info -> obj = let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in + let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 1492cfb4e4..6746eff223 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1220,7 +1220,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) + (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b026397abf..73141191cf 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -15,7 +15,6 @@ open Names open Constr open Libnames open Globnames -open Nametab open Libobject open Mod_subst @@ -228,14 +227,14 @@ let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" | CL_CONST sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_PROJ sp -> let sp = Projection.Repr.constant sp in - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_IND sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp)) let pr_class x = str (string_of_class x) @@ -520,7 +519,7 @@ module CoercionPrinting = let compare = GlobRef.Ordered.compare let encode = coercion_of_reference let subst = subst_coe_typ - let printer x = pr_global_env Id.Set.empty x + let printer x = Nametab.pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] let title = "Explicitly printed coercions: " let member_message x b = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 592057ab41..072ac9deed 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -25,7 +25,6 @@ open Termops open Namegen open Libnames open Globnames -open Nametab open Mod_subst open Decl_kinds open Context.Named.Declaration @@ -58,7 +57,7 @@ let add_name_opt na b t (nenv, env) = (* Tools for printing of Cases *) let encode_inductive r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in let constr_lengths = constructors_nrealargs indsp in (indsp,constr_lengths) @@ -97,7 +96,7 @@ module PrintingInductiveMake = let compare = ind_ord let encode = Test.encode let subst subst obj = subst_ind subst obj - let printer ind = pr_global_env Id.Set.empty (IndRef ind) + let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) let key = ["Printing";Test.field] let title = Test.title let member_message x = Test.member_message (printer x) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e49ba75b3f..89f64d328a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -29,7 +29,6 @@ open Inductive open Inductiveops open Environ open Reductionops -open Nametab open Context.Rel.Declaration type dep_flag = bool @@ -618,6 +617,6 @@ let lookup_eliminator ind_sp s = user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ Id.print id ++ strbrk ", the elimination of the inductive definition " ++ - pr_global_env Id.Set.empty (IndRef ind_sp) ++ + Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f8dc5ba4d6..5d74b59b27 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -20,7 +20,6 @@ open Util open Pp open Names open Globnames -open Nametab open Constr open Libobject open Mod_subst @@ -330,7 +329,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref description = user_err ~hdr:"object_declare" (str"Could not declare a canonical structure " ++ - (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ + (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ description)) let check_and_decompose_canonical_structure ref = diff --git a/printing/printer.ml b/printing/printer.ml index 990bdaad7d..3cf995a005 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -15,7 +15,6 @@ open Names open Constr open Environ open Globnames -open Nametab open Evd open Refiner open Constrextern @@ -242,7 +241,7 @@ let pr_abstract_cumulativity_info sigma cumi = (**********************************************************************) (* Global references *) -let pr_global_env = pr_global_env +let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty let pr_universe_instance evd inst = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5d1faf1465..388bf8efb5 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -68,7 +68,10 @@ let pf_ids_set_of_hyps gls = let pf_get_new_id id gls = next_ident_away id (pf_ids_set_of_hyps gls) -let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) +let pf_global gls id = + let env = pf_env gls in + let sigma = project gls in + Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3432ad4afa..f302960870 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,7 +34,7 @@ val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list -val pf_global : goal sigma -> Id.t -> constr +val pf_global : goal sigma -> Id.t -> evar_map * constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 148d4437fa..9f71def8fc 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -63,20 +63,20 @@ exception ConstructorWithNonParametricInductiveType of inductive exception DecidabilityIndicesNotSupported (* Some pre declaration of constant we are going to use *) -let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb_prop") +let andb_prop = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_prop") let andb_true_intro = fun _ -> - UnivGen.constr_of_global + UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_true_intro") (* We avoid to use lazy as the binding of constants can change *) -let bb () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.type") -let tt () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.true") -let ff () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.false") -let eq () = UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type") +let bb () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.type") +let tt () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.true") +let ff () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.false") +let eq () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type") -let sumbool () = UnivGen.constr_of_global (Coqlib.lib_ref "core.sumbool.type") -let andb = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb") +let sumbool () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.sumbool.type") +let andb = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb") let induct_on c = induction false None c None None let destruct_on c = destruct false None c None None @@ -873,7 +873,7 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) ) ) ) diff --git a/vernac/class.ml b/vernac/class.ml index 614b2181d9..526acd40b5 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -21,7 +21,6 @@ open Environ open Classops open Declare open Globnames -open Nametab open Decl_kinds let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -310,7 +309,7 @@ let add_coercion_hook poly local ref = | Global -> false in let () = try_add_new_coercion ref ~local poly in - let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) diff --git a/vernac/classes.ml b/vernac/classes.ml index 3cf5e9bfdf..52c1e1cf98 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -12,7 +12,6 @@ module CVars = Vars open Names open EConstr -open Nametab open CErrors open Util open Typeclasses_errors @@ -67,7 +66,7 @@ let intern_info {hint_priority;hint_pattern} = (** TODO: add subinstances *) let existing_instance glob g info = - let c = global g in + let c = Nametab.global g in let info = Option.default Hints.empty_hint_info info in let info = intern_info info in let instance, _ = Global.type_of_global_in_context (Global.env ()) c in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7b28895814..885a22b209 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -22,7 +22,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Nametab open Impargs open Reductionops open Indtypes @@ -575,6 +574,6 @@ let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 5f2818c12b..4efbb968fb 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -33,7 +33,6 @@ open Globnames open Goptions open Nameops open Termops -open Nametab open Smartlocate open Vernacexpr open Ind_tables @@ -369,7 +368,7 @@ requested | InSet -> recs ^ "_nodep" | InType -> recs ^ "t_nodep") ) in - let newid = add_suffix (basename_of_global (IndRef ind)) suffix in + let newid = add_suffix (Nametab.basename_of_global (IndRef ind)) suffix in let newref = CAst.make newid in ((newref,isdep,ind,z)::l1),l2 in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 0ac97a74e4..fbf552e649 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -266,7 +266,7 @@ let eterm_obligations env name evm fs ?status t ty = let hide_obligation () = Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - UnivGen.constr_of_global (Coqlib.lib_ref "program.tactics.obligation") + UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation") let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) diff --git a/vernac/search.ml b/vernac/search.ml index 04dcb7d565..2273130668 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -18,7 +18,6 @@ open Environ open Pattern open Libnames open Globnames -open Nametab module NamedDecl = Context.Named.Declaration @@ -192,7 +191,7 @@ let rec head_filter pat ref env sigma typ = | _ -> false let full_name_of_reference ref = - let (dir,id) = repr_path (path_of_global ref) in + let (dir,id) = repr_path (Nametab.path_of_global ref) in DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) @@ -204,14 +203,14 @@ let blacklist_filter_aux () = List.for_all is_not_bl l let module_filter (mods, outside) ref env typ = - let sp = path_of_global ref in + let sp = Nametab.path_of_global ref in let sl = dirpath sp in let is_outside md = not (is_dirpath_prefix_of md sl) in let is_inside md = is_dirpath_prefix_of md sl in if outside then List.for_all is_outside mods else List.is_empty mods || List.exists is_inside mods -let name_of_reference ref = Id.to_string (basename_of_global ref) +let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) let search_about_filter query gr env typ = match query with | GlobSearchSubPattern pat -> |