From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 25 Dec 2011 13:19:42 +0100 Subject: Imported Upstream version 8.3.pl3 --- parsing/argextend.ml4 | 4 ++-- parsing/egrammar.ml | 38 +++++++++++++++++++------------------- parsing/egrammar.mli | 4 ++-- parsing/extend.ml | 4 ++-- parsing/extend.mli | 4 ++-- parsing/extrawit.ml | 4 ++-- parsing/extrawit.mli | 4 ++-- parsing/g_constr.ml4 | 4 ++-- parsing/g_decl_mode.ml4 | 4 ++-- parsing/g_intsyntax.mli | 2 +- parsing/g_ltac.ml4 | 4 ++-- parsing/g_natsyntax.mli | 4 ++-- parsing/g_prim.ml4 | 4 ++-- parsing/g_proofs.ml4 | 4 ++-- parsing/g_tactic.ml4 | 4 ++-- parsing/g_vernac.ml4 | 4 ++-- parsing/g_xml.ml4 | 4 ++-- parsing/g_zsyntax.mli | 4 ++-- parsing/lexer.ml4 | 4 ++-- parsing/lexer.mli | 4 ++-- parsing/pcoq.ml4 | 4 ++-- parsing/pcoq.mli | 4 ++-- parsing/ppconstr.ml | 6 +++--- parsing/ppconstr.mli | 4 ++-- parsing/ppdecl_proof.ml | 4 ++-- parsing/pptactic.ml | 4 ++-- parsing/pptactic.mli | 4 ++-- parsing/ppvernac.ml | 8 ++++---- parsing/ppvernac.mli | 4 ++-- parsing/prettyp.ml | 4 ++-- parsing/prettyp.mli | 4 ++-- parsing/printer.ml | 36 +++++++++++++++++++++++------------- parsing/printer.mli | 7 ++++--- parsing/printmod.ml | 2 +- parsing/printmod.mli | 2 +- parsing/q_constr.ml4 | 4 ++-- parsing/q_coqast.ml4 | 4 ++-- parsing/q_util.ml4 | 4 ++-- parsing/q_util.mli | 4 ++-- parsing/tacextend.ml4 | 4 ++-- parsing/tactic_printer.ml | 4 ++-- parsing/tactic_printer.mli | 4 ++-- parsing/vernacextend.ml4 | 4 ++-- 43 files changed, 126 insertions(+), 115 deletions(-) (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 8bc7ad02..848223a0 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + List.fold_left (fun nb pt -> let symbs = make_constr_prod_item assoc n forpat pt in let pure_sublevels = pure_sublevels level symbs in let needed_levels = register_empty_levels forpat pure_sublevels in let pos,p4assoc,name,reinit = find_position forpat assoc level in + let nb_decls = List.length needed_levels + 1 in List.iter (prepare_empty_levels forpat) needed_levels; - grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])]) rules + grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])]; + nb_decls) 0 rules let extend_constr_notation (n,assoc,ntn,rules) = (* Add the notation in constr *) let mkact loc env = CNotation (loc,ntn,env) in let e = interp_constr_entry_key false (ETConstr (n,())) in - extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules; + let nb = extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules in (* Add the notation in cases_pattern *) let mkact loc env = CPatNotation (loc,ntn,env) in let e = interp_constr_entry_key true (ETConstr (n,())) in - extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) - true rules + let nb' = + extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) true rules in + nb+nb' (**********************************************************************) (** Making generic actions in type generic_argument *) @@ -273,7 +276,8 @@ let add_tactic_entry (key,lev,prods,tac) = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in make_rule univ (mkact key tac) make_prod_item prods in synchronize_level_positions (); - grammar_extend entry pos None [(None, None, List.rev [rules])] + grammar_extend entry pos None [(None, None, List.rev [rules])]; + 1 (**********************************************************************) (** State of the grammar extensions *) @@ -290,17 +294,17 @@ type all_grammar_command = (string * int * grammar_prod_item list * (dir_path * Tacexpr.glob_tactic_expr)) -let (grammar_state : all_grammar_command list ref) = ref [] +let (grammar_state : (int * all_grammar_command) list ref) = ref [] let extend_grammar gram = - (match gram with + let nb = match gram with | Notation (_,_,a) -> extend_constr_notation a - | TacticGrammar g -> add_tactic_entry g); - grammar_state := gram :: !grammar_state + | TacticGrammar g -> add_tactic_entry g in + grammar_state := (nb,gram) :: !grammar_state let recover_notation_grammar ntn prec = let l = map_succeed (function - | Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> + | _, Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> vars, x | _ -> failwith "") !grammar_state in @@ -320,11 +324,7 @@ let factorize_grams l1 l2 = if l1 == l2 then ([], [], l1) else list_share_tails l1 l2 let number_of_entries gcl = - List.fold_left - (fun n -> function - | Notation _ -> n + 2 (* 1 for operconstr, 1 for pattern *) - | TacticGrammar _ -> n + 1) - 0 gcl + List.fold_left (fun n (p,_) -> n + p) 0 gcl let unfreeze (grams, lex) = let (undo, redo, common) = factorize_grams !grammar_state grams in @@ -333,7 +333,7 @@ let unfreeze (grams, lex) = remove_levels n; grammar_state := common; Lexer.unfreeze lex; - List.iter extend_grammar (List.rev redo) + List.iter extend_grammar (List.rev (List.map snd redo)) let init_grammar () = remove_grammars (number_of_entries !grammar_state); diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index f6b9f6ad..8554c9be 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* c, t | _ -> c, CHole (dummy_loc, None) in - hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++ + surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) let pr_undelimited_binders sep pr_c = diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 1ad110cb..d27b318a 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* None); - hov 0 - (head ++ pr_lident (Option.get id) ++ spc() ++ + hov 1 + (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ pr_opt (pr_guard_annot bl) guard ++ str":" ++ pr_spc_lconstr c) diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index dce1bbd7..e63cf7b0 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + let mp,_,lab = repr_con kn in + str (string_of_mp mp ^ "." ^ string_of_label lab) + in + let safe_pr_ltype typ = + try str " : " ++ pr_ltype typ with _ -> mt () + in let (vars,axioms,opaque) = - Environ.ContextObjectMap.fold (fun t typ r -> + ContextObjectMap.fold (fun t typ r -> let (v,a,o) = r in match t with | Variable id -> ( Some ( @@ -521,9 +533,8 @@ let pr_assumptionset env s = | Axiom kn -> ( v , Some ( Option.default (fnl ()) a - ++ (pr_constant env kn) - ++ str " : " - ++ pr_ltype typ + ++ safe_pr_constant env kn + ++ safe_pr_ltype typ ++ fnl () ) , o @@ -531,9 +542,8 @@ let pr_assumptionset env s = | Opaque kn -> ( v , a , Some ( Option.default (fnl ()) o - ++ (pr_constant env kn) - ++ str " : " - ++ pr_ltype typ + ++ safe_pr_constant env kn + ++ safe_pr_ltype typ ++ fnl () ) ) diff --git a/parsing/printer.mli b/parsing/printer.mli index a6f73a40..99ab3ca3 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* std_ppcmds (* = pr_lconstr *) (* spiwack: printer function for sets of Environ.assumption. It is used primarily by the Print Assumption command. *) -val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds +val pr_assumptionset : + env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds type printer_pr = { diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 16f6e6c9..6339ed8f 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* MLast.patt diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 39477b0b..0d7a9cfe 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*