Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

63 lines (53 sloc) 2.158 kb
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Created by Hugo Herbelin from code formerly dispatched in
syntax_def.ml or tacinterp.ml, Sep 2009 *)
(* This file provides high-level name globalization functions *)
(* *)
open Pp
open Errors
open Libnames
open Globnames
open Misctypes
open Syntax_def
open Notation_term
let global_of_extended_global = function
| TrueGlobal ref -> ref
| SynDef kn ->
match search_syntactic_definition kn with
| [],NRef ref -> ref
| _ -> raise Not_found
let locate_global_with_alias (loc,qid) =
let ref = Nametab.locate_extended qid in
try global_of_extended_global ref
with Not_found ->
user_err_loc (loc,"",pr_qualid qid ++
str " is bound to a notation that does not denote a reference.")
let global_inductive_with_alias r =
let (loc,qid as lqid) = qualid_of_reference r in
try match locate_global_with_alias lqid with
| IndRef ind -> ind
| ref ->
user_err_loc (loc_of_reference r,"global_inductive",
pr_reference r ++ spc () ++ str "is not an inductive type.")
with Not_found -> Nametab.error_global_not_found_loc loc qid
let global_with_alias r =
let (loc,qid as lqid) = qualid_of_reference r in
try locate_global_with_alias lqid
with Not_found -> Nametab.error_global_not_found_loc loc qid
let smart_global = function
| AN r ->
global_with_alias r
| ByNotation (loc,ntn,sc) ->
Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc
let smart_global_inductive = function
| AN r ->
global_inductive_with_alias r
| ByNotation (loc,ntn,sc) ->
destIndRef
(Notation.interp_notation_as_global_reference loc isIndRef ntn sc)
Jump to Line
Something went wrong with that request. Please try again.