diff options
29 files changed, 182 insertions, 191 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 84c07dc71..947ead355 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -255,7 +255,7 @@ and ct_FORMULA_OR_INT = and ct_GRAMMAR = CT_grammar_none and ct_HINT_EXPRESSION = - CT_constructors of ct_ID + CT_constructors of ct_ID_LIST | CT_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM | CT_immediate of ct_FORMULA | CT_resolve of ct_FORMULA diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 677f7edc9..760c2286a 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -655,7 +655,7 @@ and fGRAMMAR = function | CT_grammar_none -> fNODE "grammar_none" 0 and fHINT_EXPRESSION = function | CT_constructors(x1) -> - fID x1; + fID_LIST x1; fNODE "constructors" 1 | CT_extern(x1, x2, x3) -> fINT x1; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 6fd12a010..c3355b61b 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1366,13 +1366,13 @@ let xlate_vernac = | HintsUnfold [Some id_name, q] -> (* = Old HintUnfold *) CT_hint(xlate_ident id_name, dblist, CT_unfold_hint (loc_qualid_to_ct_ID q)) - | HintsConstructors (id_name, q) -> + | HintsConstructors (Some id_name, ql) -> CT_hint(xlate_ident id_name, dblist, - CT_constructors (loc_qualid_to_ct_ID q)) - | HintsExtern (id_name, n, c, t) -> + CT_constructors (CT_id_list(List.map loc_qualid_to_ct_ID ql))) + | HintsExtern (Some id_name, n, c, t) -> CT_hint(xlate_ident id_name, dblist, CT_extern(CT_int n, xlate_formula c, xlate_tactic t)) - | HintsResolve l -> (* = Old HintsResolve *) + | HintsResolve l -> (* = Old HintsResolve *) let l = List.map (function (None,CRef r) -> r | _ -> failwith "") l in let n1, names = match List.map tac_qualid_to_ct_ID l with n1 :: names -> n1, names @@ -1380,7 +1380,7 @@ let xlate_vernac = CT_hints(CT_ident "Resolve", CT_id_ne_list(n1, names), dblist) - | HintsImmediate l -> (* = Old HintsImmediate *) + | HintsImmediate l -> (* = Old HintsImmediate *) let l = List.map (function (None,CRef r) -> r | _ -> failwith "") l in let n1, names = match List.map tac_qualid_to_ct_ID l with n1 :: names -> n1, names @@ -1388,7 +1388,7 @@ let xlate_vernac = CT_hints(CT_ident "Immediate", CT_id_ne_list(n1, names), dblist) - | HintsUnfold l -> (* = Old HintsUnfold *) + | HintsUnfold l -> (* = Old HintsUnfold *) let l = List.map (function (None,ref) -> loc_qualid_to_ct_ID ref @@ -1398,7 +1398,8 @@ let xlate_vernac = | _ -> failwith "" in CT_hints(CT_ident "Unfold", CT_id_ne_list(n1, names), - dblist)) + dblist) + | _ -> xlate_error"TODO: Hint") | VernacEndProof (Proved (true,None)) -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE) | VernacEndProof (Proved (false,None)) -> @@ -1676,7 +1677,7 @@ let xlate_vernac = | (VernacGlobalCheck _|VernacPrintOption _| VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)| VernacSetOption (_, _)|VernacUnsetOption _| - VernacHintDestruct (_, _, _, _, _, _)|VernacBack _|VernacRestoreState _| + VernacBack _|VernacRestoreState _| VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _| VernacImport (_, _)|VernacExactProof _|VernacDistfix _| VernacTacticGrammar _|VernacVar _|VernacTime _|VernacProof _) diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index 3a3fb0640..55ad8023f 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.v @@ -25,8 +25,8 @@ Variable Azero : A. is a good choice. The proof of A_eq_prop is in this case easy. *) Variable Aeq : A -> A -> bool. -Infix 4 "+" Aplus V8only 40 (left associativity). -Infix 4 "*" Amult V8only 30 (left associativity). +Infix 4 "+" Aplus V8only 50 (left associativity). +Infix 4 "*" Amult V8only 40 (left associativity). Notation "0" := Azero. Notation "1" := Aone. @@ -146,16 +146,16 @@ Variable Azero : A. Variable Aopp : A -> A. Variable Aeq : A -> A -> bool. -Infix 4 "+" Aplus V8only 40 (left associativity). -Infix 4 "*" Amult V8only 30 (left associativity). +Infix 4 "+" Aplus V8only 50 (left associativity). +Infix 4 "*" Amult V8only 40 (left associativity). Notation "0" := Azero. Notation "1" := Aone. Notation "- 0" := (Aopp Azero) (at level 0) - V8only (at level 40, left associativity). + V8only (at level 50, left associativity). Notation "- 1" := (Aopp Aone) (at level 0) - V8only (at level 40, left associativity). + V8only (at level 50, left associativity). Notation "- x" := (Aopp x) (at level 0) - V8only (at level 40, left associativity). + V8only (at level 50, left associativity). Record Ring_Theory : Prop := { Th_plus_sym : (n,m:A) n + m == m + n; diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index 8b9ae52f0..c97536846 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -31,16 +31,16 @@ Variable Azero : A. Variable Aopp : A -> A. Variable Aeq : A -> A -> bool. -Infix 4 "+" Aplus V8only 40 (left associativity). -Infix 4 "*" Amult V8only 30 (left associativity). +Infix 4 "+" Aplus V8only 50 (left associativity). +Infix 4 "*" Amult V8only 40 (left associativity). Notation "0" := Azero. Notation "1" := Aone. Notation "- 0" := (Aopp Azero) (at level 0) - V8only (at level 40, left associativity). + V8only (at level 50, left associativity). Notation "- 1" := (Aopp Aone) (at level 0) - V8only (at level 40, left associativity). + V8only (at level 50, left associativity). Notation "- x" := (Aopp x) (at level 0) - V8only (at level 40, left associativity). + V8only (at level 50, left associativity). Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2. Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2. diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 3337fbc0b..fad041f20 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -220,7 +220,10 @@ END (* Grammar extensions *) (* automatic translation of levels *) -let adapt_level n = n*10 +let adapt_level n = + if n >= 10 then n*10 else + [| 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100|].(n) + let map_modl = function | SetItemLevel(ids,NumLevel n) -> SetItemLevel(ids,NumLevel (adapt_level n)) | SetLevel n -> SetLevel(adapt_level n) diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index d11d982ff..d5d1db939 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -174,7 +174,8 @@ GEXTEND Gram | "100" RIGHTA [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,c2) | c1 = operconstr; ":"; c2 = operconstr -> CCast(loc,c1,c2) ] - | "80" RIGHTA + | "99" RIGHTA [ ] + | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) | c1 = operconstr; "->"; c2 = operconstr -> CArrow(loc,c1,c2) ] | "10" LEFTA diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1cc9f038f..c462c3bdc 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -92,7 +92,7 @@ GEXTEND Gram hyptyp = Constr.constr_pattern; pri = natural; "["; tac = tactic; "]" -> - VernacHintDestruct (local,id,dloc,hyptyp,pri,tac) + VernacHints(local,[],HintsDestruct (id,pri,dloc,hyptyp,tac)) | IDENT "Hint"; local = locality; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint @@ -115,9 +115,10 @@ GEXTEND Gram [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c] | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c] | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid] - | IDENT "Constructors"; c = global -> fun n -> HintsConstructors (n,c) + | IDENT "Constructors"; c = global -> fun n -> + HintsConstructors (Some n,[c]) | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic -> - fun name -> HintsExtern (name,n,c,tac) ] ] + fun name -> HintsExtern (Some name,n,c,tac) ] ] ; hints: [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases -> diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4 index eb1b3e466..7d75cf4cb 100644 --- a/parsing/g_proofsnew.ml4 +++ b/parsing/g_proofsnew.ml4 @@ -85,21 +85,8 @@ GEXTEND Gram | IDENT "Go"; IDENT "next" -> VernacGo GoNext | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) - - | IDENT "HintDestruct"; - local = locality; - dloc = destruct_location; - id = base_ident; - hyptyp = Constr.constr_pattern; - pri = natural; - "["; tac = tactic; "]" -> - VernacHintDestruct (local,id,dloc,hyptyp,pri,tac) - - | IDENT "Hint"; local = locality; hintname = base_ident; - dbnames = opt_hintbases; ":="; h = hint -> - VernacHints (local,dbnames, h hintname) - - | IDENT "Hints"; local = locality; (dbnames,h) = hints -> + | IDENT "Hint"; local = locality; h = hint; + dbnames = opt_hintbases -> VernacHints (local,dbnames, h) @@ -113,20 +100,24 @@ GEXTEND Gram [ [ IDENT "Local" -> true | -> false ] ] ; hint: - [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c] - | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c] - | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid] - | IDENT "Constructors"; c = global -> fun n -> HintsConstructors (n,c) - | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic -> - fun name -> HintsExtern (name,n,c,tac) ] ] - ; - hints: - [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases -> - (dbnames, HintsResolve (List.map (fun qid -> (None, CRef qid)) l)) - | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases -> - (dbnames, HintsImmediate (List.map (fun qid -> (None, CRef qid)) l)) - | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases -> - (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ] + [ [ IDENT "Resolve"; lc = LIST1 Constr.constr -> + HintsResolve (List.map (fun c -> (None, c)) lc) + | IDENT "Immediate"; lc = LIST1 Constr.constr -> + HintsImmediate (List.map (fun c -> (None,c)) lc) + | IDENT "Unfold"; lqid = LIST1 global -> + HintsUnfold (List.map (fun g -> (None,g)) lqid) + | IDENT "Constructors"; lc = LIST1 global -> + HintsConstructors (None,lc) + | IDENT "Extern"; n = natural; c = Constr.constr_pattern ; "=>"; + tac = tactic -> + HintsExtern (None,n,c,tac) + | IDENT"Destruct"; + id = base_ident; ":="; + pri = natural; + dloc = destruct_location; + hyptyp = Constr.constr_pattern; + "=>"; tac = tactic -> + HintsDestruct(id,pri,dloc,hyptyp,tac) ] ] ; constr_body: [ [ ":="; c = lconstr -> c diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 90ef93d89..9e718cfd6 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -499,7 +499,7 @@ GEXTEND Gram VernacRemoveLoadPath dir (* Type-Checking (pas dans le refman) *) - | "Type"; c = constr -> VernacGlobalCheck c + | "Type"; c = lconstr -> VernacGlobalCheck c (* Printing (careful factorization of entries) *) | IDENT "Print"; p = printable -> VernacPrint p @@ -574,9 +574,9 @@ GEXTEND Gram VernacRemoveOption (PrimaryTable table, v) ] ] ; check_command: (* TODO: rapprocher Eval et Check *) - [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = constr -> + [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> fun g -> VernacCheckMayEval (Some r, g, c) - | IDENT "Check"; c = constr -> + | IDENT "Check"; c = lconstr -> fun g -> VernacCheckMayEval (None, g, c) ] ] ; printable: diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 8d1d189ba..152141bfa 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -545,7 +545,8 @@ let default_levels_v7 = let default_levels_v8 = [200,Gramext.RightA; 100,Gramext.RightA; - 80,Gramext.RightA; + 99,Gramext.RightA; + 90,Gramext.RightA; 10,Gramext.LeftA; 9,Gramext.RightA; 1,Gramext.LeftA; diff --git a/tactics/auto.ml b/tactics/auto.ml index 4683ce144..de23d854b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -434,14 +434,16 @@ let forward_intern_tac = let set_extern_intern_tac f = forward_intern_tac := f -let add_hints local dbnames h = - let dbnames = if dbnames = [] then ["core"] else dbnames in match h with +let add_hints local dbnames0 h = + let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in + match h with | HintsResolve lhints -> let env = Global.env() and sigma = Evd.empty in let f (n,c) = let c = Constrintern.interp_constr sigma env c in let n = match n with - | None -> id_of_global (reference_of_constr c) + | None -> (*id_of_global (reference_of_constr c)*) + id_of_string "<anonymous hint>" | Some n -> n in (n,c) in add_resolves env sigma (List.map f lhints) local dbnames @@ -450,7 +452,8 @@ let add_hints local dbnames h = let f (n,c) = let c = Constrintern.interp_constr sigma env c in let n = match n with - | None -> id_of_global (reference_of_constr c) + | None -> (*id_of_global (reference_of_constr c)*) + id_of_string "<anonymous hint>" | Some n -> n in (n,c) in add_trivials env sigma (List.map f lhints) local dbnames @@ -462,17 +465,28 @@ let add_hints local dbnames h = | Some n -> n in (n,r) in add_unfolds (List.map f lhints) local dbnames - | HintsConstructors (hintname, qid) -> - let env = Global.env() and sigma = Evd.empty in - let isp = global_inductive qid in - let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in - let lcons = list_tabulate (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in - let lcons = List.map2 (fun id c -> (id,c)) (Array.to_list consnames) lcons in - add_resolves env sigma lcons local dbnames + | HintsConstructors (hintname, lqid) -> + let add_one qid = + let env = Global.env() and sigma = Evd.empty in + let isp = global_inductive qid in + let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in + let lcons = list_tabulate + (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in + let lcons = List.map2 + (fun id c -> (id,c)) (Array.to_list consnames) lcons in + add_resolves env sigma lcons local dbnames in + List.iter add_one lqid | HintsExtern (hintname, pri, patcom, tacexp) -> + let hintname = match hintname with + Some h -> h + | _ -> id_of_string "<anonymous hint>" in let pat = Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in let tacexp = !forward_intern_tac (fst pat) tacexp in add_externs hintname pri pat tacexp local dbnames + | HintsDestruct(na,pri,loc,pat,code) -> + if dbnames0<>[] then + warn (str"Database selection not implemented for destruct hints"); + Dhyp.add_destructor_hint local na loc pat pri code (**************************************************************************) (* Functions for printing the hints *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6f87f1016..276e033ac 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -125,7 +125,8 @@ let add_rewrite_hint name ort t lcsr = let f c = Constrintern.interp_constr sigma env c, ort, t in add_rew_rules name (List.map f lcsr) -VERNAC COMMAND EXTEND HintRewrite +(* V7 *) +VERNAC COMMAND EXTEND HintRewrite_v7 [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) ] -> [ add_rewrite_hint b o Tacexpr.TacId l ] | [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) @@ -133,6 +134,16 @@ VERNAC COMMAND EXTEND HintRewrite [ add_rewrite_hint b o t l ] END +(* V8 *) +VERNAC COMMAND EXTEND HintRewrite + [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] -> + [ add_rewrite_hint b o Tacexpr.TacId l ] +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) + ":" preident(b) ] -> + [ add_rewrite_hint b o t l ] +END + + (* Refine *) open Refine diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index e2ff55b23..984bd77c4 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -174,7 +174,7 @@ Definition negb := [b:bool]Cases b of Infix "||" orb (at level 4, left associativity) : bool_scope. Infix "&&" andb (at level 3, no associativity) : bool_scope - V8only (at level 30, left associativity). + V8only (at level 40, left associativity). Notation "- b" := (negb b) : bool_scope V8only. Open Local Scope bool_scope. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 680b1e20e..4c284818b 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -126,19 +126,19 @@ Definition all := [A:Type][P:A->Prop](x:A)(P x). V7only [ Notation Ex := (ex ?). ]. Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) : type_scope - V8only "'exists' x | p" (at level 200, x ident, p at level 80). + V8only "'exists' x | p" (at level 200, x ident, p at level 99). Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) : type_scope - V8only "'exists' x : t | p" (at level 200, x ident, p at level 80). + V8only "'exists' x : t | p" (at level 200, x ident, p at level 99). V7only [ Notation Ex2 := (ex2 ?). ]. Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) (at level 10, p, q at level 8) : type_scope - V8only "'exists2' x | p & q" (at level 200, x ident, p, q at level 80). + V8only "'exists2' x | p & q" (at level 200, x ident, p, q at level 99). Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) (at level 10, p, q at level 8) : type_scope V8only "'exists2' x : t | p & q" - (at level 200, x ident, t at level 200, p, q at level 80). + (at level 200, x ident, t at level 200, p, q at level 99). V7only [Notation All := (all ?). Notation "'ALL' x | p" := (all ? [x]p) diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index 102e67db6..f95f56d37 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -24,17 +24,17 @@ Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8) V7only [ Notation Ex := (ex ?). ]. Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) - V8only "'exists' x , p" (at level 200, x at level 80). + V8only "'exists' x , p" (at level 200, x at level 99). Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) - V8only "'exists' x : t , p" (at level 200, x at level 80). + V8only "'exists' x : t , p" (at level 200, x at level 99). V7only [ Notation Ex2 := (ex2 ?). ]. Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) (at level 10, p, q at level 8) - V8only "'exists2' x , p & q" (at level 200, x at level 80). + V8only "'exists2' x , p & q" (at level 200, x at level 99). Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) (at level 10, p, q at level 8) - V8only "'exists2' x : t , p & q" (at level 200, x at level 80). + V8only "'exists2' x : t , p & q" (at level 200, x at level 99). V7only[ (** Parsing only of things in [Logic.v] *) diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 8a107f5c0..149c75751 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -18,7 +18,7 @@ Uninterpreted Notation "x \/ y" (at level 7, right associativity). Uninterpreted Notation "x <-> y" (at level 8, right associativity). Uninterpreted Notation "~ x" (at level 5, right associativity) - V8only (at level 55, right associativity). + V8only (at level 75, right associativity). (** Notations for equality and inequalities *) @@ -34,28 +34,28 @@ Uninterpreted Notation "x <> y :> T" Uninterpreted Notation "x <> y" (at level 5, no associativity). -Uninterpreted V8Notation "x <= y" (at level 50, no associativity). -Uninterpreted V8Notation "x < y" (at level 50, no associativity). -Uninterpreted V8Notation "x >= y" (at level 50, no associativity). -Uninterpreted V8Notation "x > y" (at level 50, no associativity). +Uninterpreted V8Notation "x <= y" (at level 70, no associativity). +Uninterpreted V8Notation "x < y" (at level 70, no associativity). +Uninterpreted V8Notation "x >= y" (at level 70, no associativity). +Uninterpreted V8Notation "x > y" (at level 70, no associativity). -Uninterpreted V8Notation "x <= y <= z" (at level 50, y at next level). -Uninterpreted V8Notation "x <= y < z" (at level 50, y at next level). -Uninterpreted V8Notation "x < y < z" (at level 50, y at next level). -Uninterpreted V8Notation "x < y <= z" (at level 50, y at next level). +Uninterpreted V8Notation "x <= y <= z" (at level 70, y at next level). +Uninterpreted V8Notation "x <= y < z" (at level 70, y at next level). +Uninterpreted V8Notation "x < y < z" (at level 70, y at next level). +Uninterpreted V8Notation "x < y <= z" (at level 70, y at next level). (** Arithmetical notations (also used for type constructors) *) Uninterpreted Notation "x * y" (at level 3, right associativity) - V8only (at level 30, left associativity). -Uninterpreted V8Notation "x / y" (at level 30, left associativity). + V8only (at level 40, left associativity). +Uninterpreted V8Notation "x / y" (at level 40, left associativity). Uninterpreted Notation "x + y" (at level 4, left associativity). Uninterpreted Notation "x - y" (at level 4, left associativity). -Uninterpreted Notation "- x" (at level 0) V8only (at level 40). +Uninterpreted Notation "- x" (at level 0) V8only (at level 50). Uninterpreted Notation "/ x" (at level 0) - V8only (at level 30, left associativity). + V8only (at level 40, left associativity). -Uninterpreted V8Notation "x ^ y" (at level 20, left associativity). +Uninterpreted V8Notation "x ^ y" (at level 30, left associativity). (** Notations for pairs *) @@ -68,38 +68,38 @@ Uninterpreted Notation "( x , y )" (at level 0) Uninterpreted Notation "B + { x : A | P }" (at level 4, left associativity, only parsing) - V8only (at level 40, x at level 80, left associativity, only parsing). + V8only (at level 50, x at level 99, left associativity, only parsing). Uninterpreted Notation "B + { x : A | P & Q }" (at level 4, left associativity, only parsing) - V8only (at level 40, x at level 80, left associativity, only parsing). + V8only (at level 50, x at level 99, left associativity, only parsing). Uninterpreted Notation "B + { x : A & P }" (at level 4, left associativity, only parsing) - V8only (at level 40, x at level 80, left associativity, only parsing). + V8only (at level 50, x at level 99, left associativity, only parsing). Uninterpreted Notation "B + { x : A & P & Q }" (at level 4, left associativity, only parsing) - V8only (at level 40, x at level 80, left associativity, only parsing). + V8only (at level 50, x at level 99, left associativity, only parsing). (* At level 1 to factor with {x:A|P} etc *) Uninterpreted Notation "{ A } + { B }" (at level 1) - V8only (at level 0, A at level 80). + V8only (at level 0, A at level 99). Uninterpreted Notation "A + { B }" (at level 4, left associativity) - V8only (at level 40, B at level 80, left associativity). + V8only (at level 50, B at level 99, left associativity). (** Notations for sigma-types or subsets *) Uninterpreted Notation "{ x : A | P }" (at level 1) - V8only (at level 0, x at level 80). + V8only (at level 0, x at level 99). Uninterpreted Notation "{ x : A | P & Q }" (at level 1) - V8only (at level 0, x at level 80). + V8only (at level 0, x at level 99). Uninterpreted Notation "{ x : A & P }" (at level 1) - V8only (at level 0, x at level 80). + V8only (at level 0, x at level 99). Uninterpreted Notation "{ x : A & P & Q }" (at level 1) - V8only (at level 0, x at level 80). + V8only (at level 0, x at level 99). Delimits Scope type_scope with T. diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 4168655fe..50b203d4e 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -20,7 +20,7 @@ Set Implicit Arguments. Inductive list : Set := nil : list | cons : A -> list -> list. Infix "::" cons (at level 7, right associativity) : list_scope - V8only (at level 45, right associativity). + V8only (at level 60, right associativity). Open Scope list_scope. @@ -44,7 +44,7 @@ Fixpoint app [l:list] : list -> list end. Infix RIGHTA 7 "^" app : list_scope - V8only RIGHTA 45 "++". + V8only RIGHTA 60 "++". Lemma app_nil_end : (l:list)l=(l^nil). Proof. @@ -635,8 +635,8 @@ V7only [Implicits nil [].]. (** Exporting list notations *) -V8Infix "::" cons (at level 45, right associativity) : list_scope. +V8Infix "::" cons (at level 60, right associativity) : list_scope. -Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45 "++". +Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 60 "++". Open Scope list_scope. diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v index 55912fdda..00d7a032d 100644 --- a/theories/Num/NSyntax.v +++ b/theories/Num/NSyntax.v @@ -10,12 +10,12 @@ Require Export Params. -Infix 6 "<" lt V8only 50. -Infix 6 "<=" le V8only 50. -Infix 6 ">" gt V8only 50. -Infix 6 ">=" ge V8only 50. +Infix 6 "<" lt V8only 70. +Infix 6 "<=" le V8only 70. +Infix 6 ">" gt V8only 70. +Infix 6 ">=" ge V8only 70. -(*i Infix 7 "+" plus V8only 40. i*) +(*i Infix 7 "+" plus V8only 50. i*) Grammar constr lassoc_constr4 := squash_sum diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v index 0e0029422..ff5bc3e67 100644 --- a/theories/Num/NeqDef.v +++ b/theories/Num/NeqDef.v @@ -15,7 +15,7 @@ Require EqParams. Require EqAxioms. Definition neq : N -> N -> Prop := [x,y] ~(x=y). -Infix 6 "<>" neq V8only 50. +Infix 6 "<>" neq V8only 70. (* Proofs of axioms *) Lemma eq_not_neq : (x,y:N)x=y->~(x<>y). diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v index 7f7a5139e..4b7677166 100644 --- a/theories/Num/NeqParams.v +++ b/theories/Num/NeqParams.v @@ -15,7 +15,7 @@ Require Export Params. Parameter neq : N -> N -> Prop. -Infix 6 "<>" neq V8only 50. +Infix 6 "<>" neq V8only 70. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 88fd935b1..b8c5c2f4c 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -35,7 +35,7 @@ V8Infix "-" minus_fct : Rfun_scope. V8Infix "/" div_fct : Rfun_scope. Notation Local "f1 'o' f2" := (comp f1 f2) (at level 2, right associativity) : Rfun_scope - V8only (at level 15, right associativity). + V8only (at level 20, right associativity). V8Notation "/ x" := (inv_fct x) : Rfun_scope. Delimits Scope Rfun_scope with F. diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 95d60efeb..3929acdf9 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -210,33 +210,32 @@ Infix "<" Rlt (at level 5, no associativity) : R_scope. Infix ">=" Rge (at level 5, no associativity) : R_scope. Infix ">" Rgt (at level 5, no associativity) : R_scope. Infix "+" Rplus (at level 4) : R_scope - V8only (at level 40, left associativity). + V8only (at level 50, left associativity). Infix "-" Rminus (at level 4) : R_scope - V8only (at level 40, left associativity). + V8only (at level 50, left associativity). Infix "*" Rmult (at level 3) : R_scope - V8only (at level 30, left associativity). + V8only (at level 40, left associativity). Infix "/" Rdiv (at level 3) : R_scope - V8only (at level 30, left associativity). -Notation "- x" := (Ropp x) (at level 0) : R_scope V8only (at level 40, left associativity). +Notation "- x" := (Ropp x) (at level 0) : R_scope + V8only (at level 50, left associativity). Notation "x == y == z" := (eqT R x y)/\(eqT R y z) (at level 5, y at level 4, no associtivity): R_scope - V8only "x = y = z" (at level 50, y at next level, no associativity). + V8only "x = y = z" (at level 70, y at next level, no associativity). Notation "x <= y <= z" := (Rle x y)/\(Rle y z) (at level 5, y at level 4) : R_scope - V8only (at level 50, y at next level, no associativity). + V8only (at level 70, y at next level, no associativity). Notation "x <= y < z" := (Rle x y)/\(Rlt y z) (at level 5, y at level 4) : R_scope - V8only (at level 50, y at next level, no associativity). + V8only (at level 70, y at next level, no associativity). Notation "x < y < z" := (Rlt x y)/\(Rlt y z) (at level 5, y at level 4) : R_scope - V8only (at level 50, y at next level, no associativity). + V8only (at level 70, y at next level, no associativity). Notation "x < y <= z" := (Rlt x y)/\(Rle y z) (at level 5, y at level 4) : R_scope - V8only (at level 50, y at next level, no associativity). -(*Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope.*) + V8only (at level 70, y at next level, no associativity). Notation "/ x" := (Rinv x) (at level 0): R_scope - V8only (at level 30, left associativity). + V8only (at level 40, left associativity). Open Local Scope R_scope. End R_scope. diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index d5055507b..2805406a3 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -240,18 +240,18 @@ Infix NONA 5 ">" Zgt : Z_scope. Infix NONA 5 "?=" Zcompare : Z_scope. Notation "x <= y <= z" := (Zle x y)/\(Zle y z) (at level 5, y at level 4):Z_scope - V8only (at level 50, y at next level). + V8only (at level 70, y at next level). Notation "x <= y < z" := (Zle x y)/\(Zlt y z) (at level 5, y at level 4):Z_scope - V8only (at level 50, y at next level). + V8only (at level 70, y at next level). Notation "x < y < z" := (Zlt x y)/\(Zlt y z) (at level 5, y at level 4):Z_scope - V8only (at level 50, y at next level). + V8only (at level 70, y at next level). Notation "x < y <= z" := (Zlt x y)/\(Zle y z) (at level 5, y at level 4):Z_scope - V8only (at level 50, y at next level). + V8only (at level 70, y at next level). Notation "x = y = z" := x=y/\y=z : Z_scope - V8only (at level 50, y at next level). + V8only (at level 70, y at next level). (* Now a polymorphic notation Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope. diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 68d80e890..43be52419 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -1537,7 +1537,7 @@ Definition Zcompare := [x,y:Z] | (NEG x') (NEG y') => (Op (compare x' y' EGAL)) end. -V8Infix "?=" Zcompare (at level 50, no associativity) : Z_scope. +V8Infix "?=" Zcompare (at level 70, no associativity) : Z_scope. Open Local Scope Z_scope. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3f979d9b1..9c248e9dc 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1168,8 +1168,6 @@ let interp c = match c with (* Commands *) | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints - | VernacHintDestruct (local,id,l,p,n,tac) -> - Dhyp.add_destructor_hint local id l p n tac | VernacSyntacticDefinition (id,c,n) -> vernac_syntactic_definition id c n | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l | VernacReserve (idl,c) -> vernac_reserve idl c diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 441244caf..61d468fe5 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -98,8 +98,10 @@ type hints = | HintsResolve of (identifier option * constr_expr) list | HintsImmediate of (identifier option * constr_expr) list | HintsUnfold of (identifier option * reference) list - | HintsConstructors of identifier * reference - | HintsExtern of identifier * int * raw_constr_expr * raw_tactic_expr + | HintsConstructors of identifier option * reference list + | HintsExtern of identifier option * int * raw_constr_expr * raw_tactic_expr + | HintsDestruct of identifier * + int * (bool,unit) location * constr_expr * raw_tactic_expr type search_restriction = | SearchInside of reference list @@ -235,8 +237,6 @@ type vernac_expr = | VernacDeclareTacticDefinition of rec_flag * (identifier located * raw_tactic_expr) list | VernacHints of locality_flag * string list * hints - | VernacHintDestruct of locality_flag * - identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr | VernacSyntacticDefinition of identifier * constr_expr * int option | VernacDeclareImplicits of reference * explicitation list option | VernacReserve of identifier list * constr_expr diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 662649add..547477f14 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -37,8 +37,8 @@ let llambda = 200 let lif = 200 let lletin = 200 let lfix = 200 -let larrow = 80 -let lnegint = 40 +let larrow = 90 +let lnegint = 50 let lcast = 100 let lapp = 10 let ltop = (200,E) diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index c03994958..363593d78 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -213,58 +213,34 @@ let pr_opt_hintbases l = match l with | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z let pr_hints local db h pr_c = - let db_name = function - | [] -> (false , mt()) - | c1::c2 -> match c1 with - | None,_ -> (false , mt()) - | Some name,_ -> (true , pr_id name) in let opth = pr_opt_hintbases db in let pr_aux = function | CAppExpl (_,(_,qid),[]) -> pr_reference qid | _ -> mt () in - match h with + let pph = + match h with | HintsResolve l -> - let (f,dbn) = db_name l in - if f then - hov 1 (str"Hint " ++ pr_locality local ++ dbn ++ spc() ++ opth ++ - str" :=" ++ spc() ++ str"Resolve" ++ spc() ++ - prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l)) - else hov 1 - (str"Hints " ++ pr_locality local ++ str "Resolve " ++ - prlist_with_sep sep pr_aux - (List.map (fun (_,y) -> y) l) ++ spc() ++ opth) + str "Resolve " ++ + prlist_with_sep sep pr_c (List.map snd l) | HintsImmediate l -> - let (f,dbn) = db_name l in - if f then - hov 1 (str"Hint " ++ pr_locality local ++ dbn ++ spc() ++ opth ++ - str" :=" ++ spc() ++ str"Immediate" ++ spc() ++ - prlist_with_sep sep pr_c (List.map (fun (_,y) -> y) l)) - else hov 1 - (str"Hints " ++ pr_locality local ++ str "Immediate " ++ - prlist_with_sep sep pr_aux - (List.map (fun (_,y) -> y) l) ++ spc() ++ opth) + str"Immediate" ++ spc() ++ + prlist_with_sep sep pr_c (List.map snd l) | HintsUnfold l -> - let (f,dbn) = db_name l in - if f then - hov 1 (str"Hint" ++ spc() ++ pr_locality local ++ - dbn ++ spc() ++ opth ++ - str" :=" ++ spc() ++ str"Unfold" ++ spc() ++ - prlist_with_sep sep pr_reference - (List.map snd l)) - else hov 1 - (str"Hints " ++ pr_locality local ++ str "Unfold " ++ - prlist_with_sep sep pr_reference - (List.map snd l) ++ spc() ++ opth) + str "Unfold " ++ + prlist_with_sep sep pr_reference (List.map snd l) | HintsConstructors (n,c) -> - hov 1 (str"Hint " ++ pr_locality local ++ - pr_id n ++ spc() ++ opth ++ str" :=" ++ - spc() ++ str"Constructors" ++ spc() ++ pr_reference c) + str"Constructors" ++ spc() ++ + prlist_with_sep spc pr_reference c | HintsExtern (name,n,c,tac) -> - hov 1 (str"Hint " ++ pr_locality local ++ - pr_id name ++ spc() ++ opth ++ str" :=" ++ - spc() ++ str"Extern " ++ int n ++ spc() ++ pr_c c ++ - spc() ++ pr_raw_tactic tac) - + str "Extern" ++ spc() ++ int n ++ spc() ++ pr_c c ++ str" =>" ++ + spc() ++ pr_raw_tactic tac + | HintsDestruct(name,i,loc,c,tac) -> + str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++ + hov 0 (int i ++ spc() ++ pr_destruct_location loc ++ spc() ++ + pr_c c ++ str " :=") ++ spc() ++ + pr_raw_tactic tac in + hov 2 (str"Hint "++pr_locality local ++ pph ++ opth) + let pr_with_declaration pr_c = function | CWith_Definition (id,c) -> let p = pr_c c in @@ -966,11 +942,6 @@ let rec pr_vernac = function (* Rec by default *) str "Ltac ") ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr - | VernacHintDestruct (local,id,loc,c,i,tac) -> - hov 2 (str"HintDestruct " ++ pr_locality local ++ - pr_destruct_location loc ++ spc() ++ - pr_id id ++ pr_constrarg c ++ pr_intarg i ++ spc() ++ - str"[" ++ pr_raw_tactic tac ++ str"]") | VernacSyntacticDefinition (id,c,None) -> hov 2 (str"Syntactic Definition " ++ pr_id id ++ str" :=" ++ pr_lconstrarg c) |