summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml58
-rw-r--r--interp/constrextern.mli4
-rw-r--r--interp/constrintern.ml31
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/coqlib.mli2
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/dumpglob.mli2
-rw-r--r--interp/genarg.ml2
-rw-r--r--interp/genarg.mli2
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/implicit_quantifiers.mli2
-rw-r--r--interp/modintern.ml2
-rw-r--r--interp/modintern.mli2
-rw-r--r--interp/notation.ml35
-rw-r--r--interp/notation.mli2
-rw-r--r--interp/ppextend.ml2
-rw-r--r--interp/ppextend.mli2
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/reserve.mli2
-rw-r--r--interp/smartlocate.ml2
-rw-r--r--interp/smartlocate.mli2
-rw-r--r--interp/syntax_def.ml66
-rw-r--r--interp/syntax_def.mli12
-rw-r--r--interp/topconstr.ml2
-rw-r--r--interp/topconstr.mli2
26 files changed, 157 insertions, 89 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 82e3cbe1..19e1fef5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
@@ -205,7 +205,8 @@ let rec check_same_type ty1 ty2 =
| CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 ->
check_same_type a1 a2;
check_same_type b1 b2
- | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 ->
+ | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when proj1=proj2 ->
+ check_same_ref r1 r2;
List.iter2 check_same_type al1 al2
| CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
check_same_type e1 e2;
@@ -249,7 +250,7 @@ and check_same_fix_binder bl1 bl2 =
check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
| _ -> failwith "not same binder") bl1 bl2
-let same c d = try check_same_type c d; true with _ -> false
+let is_same_type c d = try let () = check_same_type c d in true with Failure _ -> false
(**********************************************************************)
(* mapping patterns to cases_pattern_expr *)
@@ -293,7 +294,7 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
if has_curly_brackets ntn
then expand_curly_brackets loc mknot ntn l
else match ntn,List.map destprim l with
- (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
+ (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
| "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
| _ ->
@@ -662,12 +663,12 @@ let rec extern inctx scopes vars r =
| GProd (loc,na,bk,t,c) ->
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
- let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
+ let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in
CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
| GLambda (loc,na,bk,t,c) ->
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
- let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
+ let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in
CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
| GCases (loc,sty,rtntypopt,tml,eqns) ->
@@ -753,30 +754,25 @@ and extern_typ (_,scopes) =
and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
-and factorize_prod scopes vars aty c =
- try
- if !Flags.raw_print or !print_no_symbol then raise No_match;
- ([],extern_symbol scopes vars c (uninterp_notations c))
- with No_match -> match c with
- | GProd (loc,(Name id as na),bk,ty,c)
- when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
- & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
- -> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
- ((loc,Name id)::nal,c)
- | c -> ([],extern_typ scopes vars c)
-
-and factorize_lambda inctx scopes vars aty c =
- try
- if !Flags.raw_print or !print_no_symbol then raise No_match;
- ([],extern_symbol (Some Notation.type_scope,snd scopes) vars c (uninterp_notations c))
- with No_match -> match c with
- | GLambda (loc,na,bk,ty,c)
- when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
- & not (occur_name na aty) (* To avoid na in ty' escapes scope *)
- -> let (nal,c) =
- factorize_lambda inctx scopes (add_vname vars na) aty c in
- ((loc,na)::nal,c)
- | c -> ([],sub_extern inctx scopes vars c)
+and factorize_prod scopes vars na bk aty c =
+ let c = extern_typ scopes vars c in
+ match na, c with
+ | Name id, CProdN (loc,[nal,Default bk',ty],c)
+ when bk = bk' && is_same_type aty ty
+ & not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
+ nal,c
+ | _ ->
+ [],c
+
+and factorize_lambda inctx scopes vars na bk aty c =
+ let c = sub_extern inctx scopes vars c in
+ match c with
+ | CLambdaN (loc,[nal,Default bk',ty],c)
+ when bk = bk' && is_same_type aty ty
+ & not (occur_name na ty) (* avoid na in ty escapes scope *) ->
+ nal,c
+ | _ ->
+ [],c
and extern_local_binder scopes vars = function
[] -> ([],[],[])
@@ -790,7 +786,7 @@ and extern_local_binder scopes vars = function
let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
(match extern_local_binder scopes (name_fold Idset.add na vars) l with
(assums,ids,LocalRawAssum(nal,k,ty')::l)
- when same ty ty' &
+ when is_same_type ty ty' &
match na with Name id -> not (occur_var_constr_expr id ty')
| _ -> true ->
(na::assums,na::ids,
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 2a53eb85..1a1560e5 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
@@ -19,7 +19,7 @@ open Pattern
open Topconstr
open Notation
-val check_same_type : constr_expr -> constr_expr -> unit
+val is_same_type : constr_expr -> constr_expr -> bool
(** Translation of pattern, cases pattern, glob_constr and term into syntax
trees for printing *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1dd735ad..45df005c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
@@ -259,8 +259,9 @@ let pr_scope_stack = function
let error_inconsistent_scope loc id scopes1 scopes2 =
user_err_loc (loc,"set_var_scope",
- pr_id id ++ str " is used both in " ++
- pr_scope_stack scopes1 ++ strbrk " and in " ++ pr_scope_stack scopes2)
+ pr_id id ++ str " is here used in " ++
+ pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++
+ pr_scope_stack scopes1)
let error_expect_constr_notation_type loc id =
user_err_loc (loc,"",
@@ -274,17 +275,17 @@ let error_expect_binder_notation_type loc id =
let set_var_scope loc id istermvar env ntnvars =
try
let idscopes,typ = List.assoc id ntnvars in
- if !idscopes <> None &
- (* scopes have no effect on the interpretation of identifiers, hence
- we can tolerate having a variable occurring several times in
- different scopes: *) typ <> NtnInternTypeIdent &
- make_current_scope (Option.get !idscopes)
- <> make_current_scope (env.tmp_scope,env.scopes) then
- error_inconsistent_scope loc id
- (make_current_scope (Option.get !idscopes))
- (make_current_scope (env.tmp_scope,env.scopes))
- else
- idscopes := Some (env.tmp_scope,env.scopes);
+ if istermvar then
+ (* scopes have no effect on the interpretation of identifiers *)
+ if !idscopes = None then
+ idscopes := Some (env.tmp_scope,env.scopes)
+ else
+ if make_current_scope (Option.get !idscopes)
+ <> make_current_scope (env.tmp_scope,env.scopes)
+ then
+ error_inconsistent_scope loc id
+ (make_current_scope (Option.get !idscopes))
+ (make_current_scope (env.tmp_scope,env.scopes));
match typ with
| NtnInternTypeBinder ->
if istermvar then error_expect_binder_notation_type loc id
@@ -1682,7 +1683,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
(push_rel d env, d::params, succ n, impls)
| Some b ->
let c = understand_judgment env b in
- let d = (na, Some c.uj_val, c.uj_type) in
+ let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in
(push_rel d env, d::params, succ n, impls))
(env,[],1,[]) (List.rev bl)
in (env, par), impls
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 7d000902..7a4bba10 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index eb7828ea..d9649976 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 5d3580f2..3dd82c28 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 07e813e7..b0a49c17 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index b02cc966..e4712cf1 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 594e8fd9..a9adbe83 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 01217204..302aa950 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index f2739043..9950178c 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index ce518a9c..5a13bfd1 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/modintern.ml b/interp/modintern.ml
index a13560c0..071fe7f8 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 71a00c2f..69f05ed1 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/notation.ml b/interp/notation.ml
index d2bee550..e3fb5d5e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
@@ -53,6 +53,9 @@ let notation_level_map = ref Gmap.empty
(* Scopes table: scope_name -> symbol_interpretation *)
let scope_map = ref Gmap.empty
+(* Delimiter table : delimiter -> scope_name *)
+let delimiters_map = ref Gmap.empty
+
let empty_scope = {
notations = Gmap.empty;
delimiters = None
@@ -74,12 +77,25 @@ let declare_scope scope =
(* Flags.if_warn message ("Creating scope "^scope);*)
scope_map := Gmap.add scope empty_scope !scope_map
+let error_unknown_scope sc = error ("Scope "^sc^" is not declared.")
+
let find_scope scope =
try Gmap.find scope !scope_map
- with Not_found -> error ("Scope "^scope^" is not declared.")
+ with Not_found -> error_unknown_scope scope
let check_scope sc = let _ = find_scope sc in ()
+(* [sc] might be here a [scope_name] or a [delimiter]
+ (now allowed after Open Scope) *)
+
+let normalize_scope sc =
+ try let _ = Gmap.find sc !scope_map in sc
+ with Not_found ->
+ try
+ let sc = Gmap.find sc !delimiters_map in
+ let _ = Gmap.find sc !scope_map in sc
+ with Not_found -> error_unknown_scope sc
+
(**********************************************************************)
(* The global stack of scopes *)
@@ -99,10 +115,13 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
(* Exportation of scopes *)
let open_scope i (_,(local,op,sc)) =
- if i=1 then begin
- (match sc with Scope sc -> check_scope sc | _ -> ());
- scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack
- end
+ if i=1 then
+ let sc = match sc with
+ | Scope sc -> Scope (normalize_scope sc)
+ | _ -> sc
+ in
+ scope_stack :=
+ if op then sc :: !scope_stack else list_except sc !scope_stack
let cache_scope o =
open_scope 1 o
@@ -142,8 +161,6 @@ let make_current_scopes (tmp_scope,scopes) =
(**********************************************************************)
(* Delimiters *)
-let delimiters_map = ref Gmap.empty
-
let declare_delimiters scope key =
let sc = find_scope scope in
let newsc = { sc with delimiters = Some key } in
@@ -361,7 +378,7 @@ let interp_prim_token_gen g loc p local_scopes =
with Not_found ->
user_err_loc (loc,"interp_prim_token",
(match p with
- | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n
+ | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
| String s -> str "No interpretation for string " ++ qs s) ++ str ".")
let interp_prim_token =
diff --git a/interp/notation.mli b/interp/notation.mli
index f429e377..2ecfbda7 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index ebf94bd8..45aab2c1 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index d3be8c49..cae644ab 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index a07f5c84..935a7269 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 97b22d2b..b57894b9 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 4e472b7a..2976f078 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 474058cc..de34f5ba 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 8863bbbd..8dfeba07 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
@@ -18,7 +18,9 @@ open Nametab
(* Syntactic definitions. *)
-let syntax_table = ref (KNmap.empty : interpretation KNmap.t)
+type version = Flags.compat_version option
+
+let syntax_table = ref (KNmap.empty : (interpretation*version) KNmap.t)
let _ = Summary.declare_summary
"SYNTAXCONSTANT"
@@ -26,14 +28,14 @@ let _ = Summary.declare_summary
Summary.unfreeze_function = (fun ft -> syntax_table := ft);
Summary.init_function = (fun () -> syntax_table := KNmap.empty) }
-let add_syntax_constant kn c =
- syntax_table := KNmap.add kn c !syntax_table
+let add_syntax_constant kn c onlyparse =
+ syntax_table := KNmap.add kn (c,onlyparse) !syntax_table
-let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
+let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
if Nametab.exists_cci sp then
errorlabstrm "cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
- add_syntax_constant kn pat;
+ add_syntax_constant kn pat onlyparse;
Nametab.push_syndef (Nametab.Until i) sp kn
let is_alias_of_already_visible_name sp = function
@@ -46,7 +48,7 @@ let is_alias_of_already_visible_name sp = function
let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
if not (is_alias_of_already_visible_name sp pat) then begin
Nametab.push_syndef (Nametab.Exactly i) sp kn;
- if not onlyparse then
+ if onlyparse = None then
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared inbetween *)
Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
@@ -62,7 +64,8 @@ let subst_syntax_constant (subst,(local,pat,onlyparse)) =
let classify_syntax_constant (local,_,_ as o) =
if local then Dispose else Substitute o
-let in_syntax_constant : bool * interpretation * bool -> obj =
+let in_syntax_constant
+ : bool * interpretation * Flags.compat_version option -> obj =
declare_object {(default_object "SYNTAXCONSTANT") with
cache_function = cache_syntax_constant;
load_function = load_syntax_constant;
@@ -80,5 +83,50 @@ 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_global r = pr_global_env Idset.empty r
+let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Idset.empty kn)
+
+let allow_compat_notations = ref true
+let verbose_compat_notations = ref false
+
+let is_verbose_compat () =
+ !verbose_compat_notations || not !allow_compat_notations
+
+let verbose_compat kn def = function
+ | Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
+ let act =
+ if !verbose_compat_notations then msg_warning else errorlabstrm ""
+ in
+ let pp_def = match def with
+ | [], ARef r -> str " is " ++ pr_global_env Idset.empty r
+ | _ -> str " is a compatibility notation"
+ in
+ let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in
+ act (pr_syndef kn ++ pp_def ++ since)
+ | _ -> ()
+
let search_syntactic_definition kn =
- out_pat (KNmap.find kn !syntax_table)
+ let pat,v = KNmap.find kn !syntax_table in
+ let def = out_pat pat in
+ verbose_compat kn def v;
+ def
+
+open Goptions
+
+let set_verbose_compat_notations =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "verbose compatibility notations";
+ optkey = ["Verbose";"Compat";"Notations"];
+ optread = (fun () -> !verbose_compat_notations);
+ optwrite = ((:=) verbose_compat_notations) }
+
+let set_compat_notations =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "accept compatibility notations";
+ optkey = ["Compat"; "Notations"];
+ optread = (fun () -> !allow_compat_notations);
+ optwrite = ((:=) allow_compat_notations) }
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index e4da52a3..036fe30a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
@@ -17,7 +17,13 @@ open Libnames
type syndef_interpretation = (identifier * subscopes) list * aconstr
-val declare_syntactic_definition : bool -> identifier -> bool ->
- syndef_interpretation -> unit
+val declare_syntactic_definition : bool -> identifier ->
+ Flags.compat_version option -> syndef_interpretation -> unit
val search_syntactic_definition : kernel_name -> syndef_interpretation
+
+(** Options concerning verbose display of compatibility notations
+ or their deactivation *)
+
+val set_verbose_compat_notations : bool -> unit
+val set_compat_notations : bool -> unit
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 04d39fbf..b02a67ea 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 79bab389..c4c775b5 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 04:47:01 +0000