From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- parsing/argextend.ml4 | 2 +- parsing/egrammar.ml | 74 ++++++++++++++---------- parsing/egrammar.mli | 14 ++++- parsing/extend.ml | 6 +- parsing/extend.mli | 4 +- parsing/extrawit.ml | 2 +- parsing/extrawit.mli | 2 +- parsing/g_constr.ml4 | 137 ++++++++++++++++++++++----------------------- parsing/g_decl_mode.ml4 | 2 +- parsing/g_ltac.ml4 | 2 +- parsing/g_natsyntax.mli | 2 +- parsing/g_prim.ml4 | 2 +- parsing/g_proofs.ml4 | 2 +- parsing/g_tactic.ml4 | 2 +- parsing/g_vernac.ml4 | 38 +++++++------ parsing/g_xml.ml4 | 2 +- parsing/g_zsyntax.mli | 2 +- parsing/lexer.ml4 | 2 +- parsing/lexer.mli | 2 +- parsing/pcoq.ml4 | 34 ++++++++--- parsing/pcoq.mli | 11 ++-- parsing/ppconstr.ml | 58 ++++++++++--------- parsing/ppconstr.mli | 2 +- parsing/ppdecl_proof.ml | 2 +- parsing/pptactic.ml | 2 +- parsing/pptactic.mli | 2 +- parsing/ppvernac.ml | 14 ++++- parsing/ppvernac.mli | 2 +- parsing/prettyp.ml | 2 +- parsing/prettyp.mli | 2 +- parsing/printer.ml | 2 +- parsing/printer.mli | 2 +- parsing/q_constr.ml4 | 2 +- parsing/q_coqast.ml4 | 9 ++- parsing/q_util.ml4 | 2 +- parsing/q_util.mli | 2 +- parsing/tacextend.ml4 | 2 +- parsing/tactic_printer.ml | 2 +- parsing/tactic_printer.mli | 2 +- parsing/vernacextend.ml4 | 2 +- 40 files changed, 258 insertions(+), 199 deletions(-) (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 6baff5da..8bc7ad02 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) +(* $Id: argextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Genarg open Q_util diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 67492e3e..943a9487 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: egrammar.ml 13329 2010-07-26 11:05:39Z herbelin $ *) open Pp open Util @@ -66,41 +66,52 @@ type grammar_constr_prod_item = type 'a action_env = 'a list * 'a list list let make_constr_action - (f : loc -> constr_expr action_env -> constr_expr) pil = - let rec make (env,envlist as fullenv : constr_expr action_env) = function + (f : loc -> constr_notation_substitution -> constr_expr) pil = + let rec make (constrs,constrlists,binders as fullsubst) = function | [] -> - Gramext.action (fun loc -> f loc fullenv) + Gramext.action (fun loc -> f loc fullsubst) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make fullenv tl) + Gramext.action (fun _ -> make fullsubst tl) | GramConstrNonTerminal (typ, Some _) :: tl -> (* parse a binding non-terminal *) - (match typ with - | (ETConstr _| ETOther _) -> - Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl) - | ETReference -> - Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl) - | ETName -> - Gramext.action (fun (na:name located) -> - make (constr_expr_of_name na :: env, envlist) tl) - | ETBigint -> - Gramext.action (fun (v:Bigint.bigint) -> - make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl) - | ETConstrList (_,n) -> - Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl) + (match typ with + | (ETConstr _| ETOther _) -> + Gramext.action (fun (v:constr_expr) -> + make (v :: constrs, constrlists, binders) tl) + | ETReference -> + Gramext.action (fun (v:reference) -> + make (CRef v :: constrs, constrlists, binders) tl) + | ETName -> + Gramext.action (fun (na:name located) -> + make (constr_expr_of_name na :: constrs, constrlists, binders) tl) + | ETBigint -> + Gramext.action (fun (v:Bigint.bigint) -> + make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl) + | ETConstrList (_,n) -> + Gramext.action (fun (v:constr_expr list) -> + make (constrs, v::constrlists, binders) tl) + | ETBinder _ | ETBinderList (true,_) -> + Gramext.action (fun (v:local_binder list) -> + make (constrs, constrlists, v::binders) tl) + | ETBinderList (false,_) -> + Gramext.action (fun (v:local_binder list list) -> + make (constrs, constrlists, List.flatten v::binders) tl) | ETPattern -> failwith "Unexpected entry of type cases pattern") | GramConstrListMark (n,b) :: tl -> (* Rebuild expansions of ConstrList *) - let heads,env = list_chop n env in - if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl - else make (env,heads::envlist) tl + let heads,constrs = list_chop n constrs in + let constrlists = + if b then (heads@List.hd constrlists)::List.tl constrlists + else heads::constrlists + in make (constrs, constrlists, binders) tl in - make ([],[]) (List.rev pil) + make ([],[],[]) (List.rev pil) let make_cases_pattern_action - (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil = - let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function + (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = + let rec make (env,envlist as fullenv) = function | [] -> Gramext.action (fun loc -> f loc fullenv) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> @@ -123,7 +134,7 @@ let make_cases_pattern_action | ETConstrList (_,_) -> Gramext.action (fun (vl:cases_pattern_expr list) -> make (env, vl :: envlist) tl) - | (ETPattern | ETOther _) -> + | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) -> failwith "Unexpected entry of type cases pattern or other") | GramConstrListMark (n,b) :: tl -> (* Rebuild expansions of ConstrList *) @@ -271,7 +282,10 @@ type notation_grammar = int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list type all_grammar_command = - | Notation of (precedence * tolerability list) * notation_grammar + | Notation of + (precedence * tolerability list) * + notation_var_internalization_type list * + notation_grammar | TacticGrammar of (string * int * grammar_prod_item list * (dir_path * Tacexpr.glob_tactic_expr)) @@ -280,14 +294,16 @@ let (grammar_state : all_grammar_command list ref) = ref [] let extend_grammar gram = (match gram with - | Notation (_,a) -> extend_constr_notation a + | Notation (_,_,a) -> extend_constr_notation a | TacticGrammar g -> add_tactic_entry g); grammar_state := gram :: !grammar_state let recover_notation_grammar ntn prec = let l = map_succeed (function - | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x - | _ -> failwith "") !grammar_state in + | Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> + vars, x + | _ -> + failwith "") !grammar_state in assert (List.length l = 1); List.hd l diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index decc263d..f6b9f6ad 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: egrammar.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) (*i*) open Util @@ -48,7 +48,12 @@ type grammar_prod_item = (* Adding notations *) type all_grammar_command = - | Notation of (precedence * tolerability list) * notation_grammar + | Notation of + (precedence * tolerability list) + * notation_var_internalization_type list + (** not needed for defining grammar, hosted by egrammar for + transmission to interp_aconstr (via recover_notation_grammar) *) + * notation_grammar | TacticGrammar of (string * int * grammar_prod_item list * (dir_path * Tacexpr.glob_tactic_expr)) @@ -64,5 +69,8 @@ val extend_vernac_command_grammar : val get_extend_vernac_grammars : unit -> (string * grammar_prod_item list list) list +(** For a declared grammar, returns the rule + the ordered entry types + of variables in the rule (for use in the interpretation) *) val recover_notation_grammar : - notation -> (precedence * tolerability list) -> notation_grammar + notation -> (precedence * tolerability list) -> + notation_var_internalization_type list * notation_grammar diff --git a/parsing/extend.ml b/parsing/extend.ml index 5e79cbd5..92ca4dd1 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extend.ml 13329 2010-07-26 11:05:39Z herbelin $ i*) open Util @@ -45,16 +45,18 @@ type production_level = type ('lev,'pos) constr_entry_key_gen = | ETName | ETReference | ETBigint + | ETBinder of bool | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string | ETConstrList of ('lev * 'pos) * Token.pattern list + | ETBinderList of bool * Token.pattern list (* Entries level (left-hand-side of grammar rules) *) type constr_entry_key = (int,unit) constr_entry_key_gen -(* Entries used in productions (in right-hand-side of grammar rules) *) +(* Entries used in productions (in right-hand side of grammar rules) *) type constr_prod_entry_key = (production_level,production_position) constr_entry_key_gen diff --git a/parsing/extend.mli b/parsing/extend.mli index 5e79cbd5..ad371872 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extend.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) open Util @@ -45,10 +45,12 @@ type production_level = type ('lev,'pos) constr_entry_key_gen = | ETName | ETReference | ETBigint + | ETBinder of bool | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string | ETConstrList of ('lev * 'pos) * Token.pattern list + | ETBinderList of bool * Token.pattern list (* Entries level (left-hand-side of grammar rules) *) type constr_entry_key = diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index e56c2e12..e12e2593 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extrawit.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Util open Genarg diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli index 02b71ddc..1a1b6fe4 100644 --- a/parsing/extrawit.mli +++ b/parsing/extrawit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extrawit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Util open Genarg diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index bba3d0d6..76b761b1 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) +(* $Id: g_constr.ml4 13359 2010-07-30 08:46:55Z herbelin $ *) open Pp open Pcoq @@ -34,11 +34,6 @@ let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty)) -let loc_of_binder_let = function - | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc - | LocalRawDef ((loc,_),_)::_ -> loc - | _ -> dummy_loc - let binders_of_lidents l = List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, @@ -88,8 +83,8 @@ let lpar_id_coloneq = | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) -let impl_ident = - Gram.Entry.of_parser "impl_ident" +let impl_ident_head = + Gram.Entry.of_parser "impl_ident_head" (fun strm -> match Stream.npeek 1 strm with | [(_,"{")] -> @@ -126,13 +121,13 @@ let ident_with = | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) -let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None +let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr sort global constr_pattern lconstr_pattern Constr.ident - binder binder_let binders_let record_declaration - binders_let_fixannot typeclass_constraint pattern appl_arg; + closed_binder open_binders binder binders binders_fixannot + record_declaration typeclass_constraint pattern appl_arg; Constr.ident: [ [ id = Prim.ident -> id @@ -204,7 +199,7 @@ GEXTEND Gram | "("; c = operconstr LEVEL "200"; ")" -> (match c with CPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> - CNotation(loc,"( _ )",([c],[])) + CNotation(loc,"( _ )",([c],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c | "`{"; c = operconstr LEVEL "200"; "}" -> @@ -214,14 +209,10 @@ GEXTEND Gram ] ] ; forall: - [ [ "forall" -> () - | IDENT "Π" -> () - ] ] + [ [ "forall" -> () ] ] ; lambda: - [ [ "fun" -> () - | IDENT "λ" -> () - ] ] + [ [ "fun" -> () ] ] ; record_declaration: [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs) @@ -234,13 +225,13 @@ GEXTEND Gram (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ] ; binder_constr: - [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" -> + [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" -> mkCProdN loc bl c - | lambda; bl = binder_list; [ "=>" | "," ]; c = operconstr LEVEL "200" -> + | lambda; bl = open_binders; [ "=>" | "," ]; c = operconstr LEVEL "200" -> mkCLambdaN loc bl c - | "let"; id=name; bl = binders_let; ty = type_cstr; ":="; + | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - let loc1 = loc_of_binder_let bl in + let loc1 = join_loc (local_binders_loc bl) (constr_loc c1) in CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in @@ -253,7 +244,7 @@ GEXTEND Gram po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - CLetTuple (loc,List.map snd lb,po,c1,c2) + CLetTuple (loc,lb,po,c1,c2) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)]) @@ -298,7 +289,7 @@ GEXTEND Gram | "cofix" -> false ] ] ; fix_decl: - [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":="; + [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":="; c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ] ; @@ -310,14 +301,14 @@ GEXTEND Gram [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ] ; pred_pattern: - [ [ ona = OPT ["as"; id=name -> snd id]; + [ [ ona = OPT ["as"; id=name -> id]; ty = OPT ["in"; t=lconstr -> t] -> (ona,ty) ] ] ; case_type: [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ] ; return_type: - [ [ a = OPT [ na = OPT["as"; id=name -> snd id]; + [ [ a = OPT [ na = OPT["as"; na=name -> na]; ty = case_type -> (na,ty) ] -> match a with | None -> None, None @@ -365,15 +356,7 @@ GEXTEND Gram | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n)) | s = string -> CPatPrim (loc, String s) ] ] ; - binder_list: - [ [ idl=LIST1 name; bl=binders_let -> - LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl - | idl=LIST1 name; ":"; c=lconstr -> - [LocalRawAssum (idl,Default Explicit,c)] - | cl = binders_let -> cl - ] ] - ; - binder_assum: + impl_ident_tail: [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None)) | idl=LIST1 name; ":"; c=lconstr; "}" -> (fun id -> LocalRawAssum (id::idl,Default Implicit,c)) @@ -390,47 +373,59 @@ GEXTEND Gram rel=OPT constr; "}" -> (id, CMeasureRec (m,rel)) ] ] ; - binders_let_fixannot: - [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot -> - (assum (loc, Name id) :: fst bl), snd bl - | f = fixannot -> [], f - | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl - | -> [], (None, CStructRec) + binders_fixannot: + [ [ id = impl_ident_head; assum = impl_ident_tail; bl = binders_fixannot -> + (assum (loc, Name id) :: fst bl), snd bl + | f = fixannot -> [], f + | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl + | -> [], (None, CStructRec) ] ] ; - binders_let: - [ [ b = binder_let; bl = binders_let -> b @ bl - | -> [] ] ] - ; - binder_let: - [ [ id=name -> - [LocalRawAssum ([id],Default Explicit,CHole (loc, None))] - | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> - [LocalRawAssum (id::idl,Default Explicit,c)] - | "("; id=name; ":"; c=lconstr; ")" -> - [LocalRawAssum ([id],Default Explicit,c)] - | "("; id=name; ":="; c=lconstr; ")" -> - [LocalRawDef (id,c)] - | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))] - | "{"; id=name; "}" -> - [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] - | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> - [LocalRawAssum (id::idl,Default Implicit,c)] - | "{"; id=name; ":"; c=lconstr; "}" -> - [LocalRawAssum ([id],Default Implicit,c)] - | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl) - | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc - | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc + open_binders: + (* Same as binders but parentheses around a closed binder are optional if + the latter is unique *) + [ [ (* open binder *) + id = name; idl = LIST0 name; ":"; c = lconstr -> + [LocalRawAssum (id::idl,Default Explicit,c)] + (* binders factorized with open binder *) + | id = name; idl = LIST0 name; bl = binders -> + let t = CHole (loc, Some (Evd.BinderType (snd id))) in + LocalRawAssum (id::idl,Default Explicit,t)::bl + | id1 = name; ".."; id2 = name -> + [LocalRawAssum ([id1;(loc,Name ldots_var);id2], + Default Explicit,CHole (loc,None))] + | bl = closed_binder; bl' = binders -> + bl@bl' ] ] ; + binders: + [ [ l = LIST0 binder -> List.flatten l ] ] + ; binder: - [ [ id=name -> ([id],Default Explicit,CHole (loc, None)) - | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) - | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c) + [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (loc, None))] + | bl = closed_binder -> bl ] ] + ; + closed_binder: + [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> + [LocalRawAssum (id::idl,Default Explicit,c)] + | "("; id=name; ":"; c=lconstr; ")" -> + [LocalRawAssum ([id],Default Explicit,c)] + | "("; id=name; ":="; c=lconstr; ")" -> + [LocalRawDef (id,c)] + | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> + [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))] + | "{"; id=name; "}" -> + [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] + | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> + [LocalRawAssum (id::idl,Default Implicit,c)] + | "{"; id=name; ":"; c=lconstr; "}" -> + [LocalRawAssum ([id],Default Implicit,c)] + | "{"; id=name; idl=LIST1 name; "}" -> + List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl) + | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc + | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc ] ] ; typeclass_constraint: diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index c9da8779..0aa8272b 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) +(* $Id: g_decl_mode.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Decl_expr diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index d5c8b78b..e0f31b98 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) +(* $Id: g_ltac.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli index 5ad93c9e..21335332 100644 --- a/parsing/g_natsyntax.mli +++ b/parsing/g_natsyntax.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: g_natsyntax.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Nice syntax for naturals. *) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 5c2fadbb..a7ed810d 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(*i $Id$ i*) +(*i $Id: g_prim.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pcoq open Names diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 779e4b22..df23465e 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) +(* $Id: g_proofs.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Pcoq diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 324119ed..4a1b9c63 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) +(* $Id: g_tactic.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Pcoq diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c3ea4d22..1f5a6cf9 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) +(* $Id: g_vernac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp @@ -134,9 +134,9 @@ GEXTEND Gram gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr; + [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr; l = LIST0 - [ "with"; id = identref; bl = binders_let; ":"; c = lconstr -> + [ "with"; id = identref; bl = binders; ":"; c = lconstr -> (Some id,(bl,c,None)) ] -> VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook) | stre = assumption_token; nl = inline; bl = assum_list -> @@ -170,7 +170,7 @@ GEXTEND Gram ; gallina_ext: [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; - ps = binders_let; + ps = binders; s = OPT [ ":"; s = lconstr -> s ]; cfs = [ ":="; l = constructor_list_or_record_decl -> l | -> RecordDecl (None, []) ] -> @@ -231,13 +231,13 @@ GEXTEND Gram ; (* Simple definitions *) def_body: - [ [ bl = binders_let; ":="; red = reduce; c = lconstr -> + [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) - | bl = binders_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> + | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) - | bl = binders_let; ":"; t = lconstr -> + | bl = binders; ":"; t = lconstr -> ProveBody (bl, t) ] ] ; reduce: @@ -254,7 +254,7 @@ GEXTEND Gram ; (* Inductives and records *) inductive_definition: - [ [ id = identref; oc = opt_coercion; indpar = binders_let; + [ [ id = identref; oc = opt_coercion; indpar = binders; c = OPT [ ":"; c = lconstr -> c ]; ":="; lc = constructor_list_or_record_decl; ntn = decl_notation -> (((oc,id),indpar,c,lc),ntn) ] ] @@ -281,13 +281,13 @@ GEXTEND Gram (* (co)-fixpoints *) rec_definition: [ [ id = identref; - bl = binders_let_fixannot; + bl = binders_fixannot; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ] ; corec_definition: - [ [ id = identref; bl = binders_let; ty = type_cstr; + [ [ id = identref; bl = binders; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> ((id,bl,ty,def),ntn) ] ] ; @@ -305,6 +305,10 @@ GEXTEND Gram IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) | IDENT "Minimality"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) + | IDENT "Elimination"; "for"; ind = smart_global; + IDENT "Sort"; s = sort-> CaseScheme(true,ind,s) + | IDENT "Case"; "for"; ind = smart_global; + IDENT "Sort"; s = sort-> CaseScheme(false,ind,s) | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] ; (* Various Binders *) @@ -324,12 +328,12 @@ GEXTEND Gram [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ] ; record_binder_body: - [ [ l = binders_let; oc = of_type_with_opt_coercion; + [ [ l = binders; oc = of_type_with_opt_coercion; t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t)) - | l = binders_let; oc = of_type_with_opt_coercion; + | l = binders; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> fun id -> (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) - | l = binders_let; ":="; b = lconstr -> fun id -> + | l = binders; ":="; b = lconstr -> fun id -> match b with | CCast(_,b, Rawterm.CastConv (_, t)) -> (false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) @@ -352,7 +356,7 @@ GEXTEND Gram ; constructor_type: - [[ l = binders_let; + [[ l = binders; t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (coe,(id,mkCProdN loc l c)) | -> @@ -527,7 +531,7 @@ GEXTEND Gram t = class_rawexpr -> VernacCoercion (use_locality_exp (), ByNotation ntn, s, t) - | IDENT "Context"; c = binders_let -> + | IDENT "Context"; c = binders -> VernacContext c | IDENT "Instance"; namesup = instance_name; ":"; @@ -577,7 +581,7 @@ GEXTEND Gram | IDENT "transparent" -> Conv_oracle.transparent ] ] ; instance_name: - [ [ name = identref; sup = OPT binders_let -> + [ [ name = identref; sup = OPT binders -> (let (loc,id) = name in (loc, Name id)), (Option.default [] sup) | -> (loc, Anonymous), [] ] ] @@ -922,6 +926,8 @@ GEXTEND Gram syntax_extension_type: [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference | IDENT "bigint" -> ETBigint + | IDENT "binder" -> ETBinder true + | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; opt_scope: diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index b75d55c5..5ad9f664 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) +(* $Id: g_xml.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli index 74637969..16b1ba65 100644 --- a/parsing/g_zsyntax.mli +++ b/parsing/g_zsyntax.mli @@ -6,6 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: g_zsyntax.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Nice syntax for integers. *) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 59b1a048..cc48c84f 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -10,7 +10,7 @@ (* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with * ast-based camlp4 *) -(*i $Id$ i*) +(*i $Id: lexer.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Util diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 35836f5c..a25774c5 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: lexer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Util diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6a85775d..90a9220f 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*) -(*i $Id$ i*) +(*i $Id: pcoq.ml4 13329 2010-07-26 11:05:39Z herbelin $ i*) open Pp open Util @@ -313,10 +313,11 @@ module Constr = let pattern = Gram.Entry.create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" let lconstr_pattern = gec_constr "lconstr_pattern" + let closed_binder = Gram.Entry.create "constr:closed_binder" let binder = Gram.Entry.create "constr:binder" - let binder_let = Gram.Entry.create "constr:binder_let" - let binders_let = Gram.Entry.create "constr:binders_let" - let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot" + let binders = Gram.Entry.create "constr:binders" + let open_binders = Gram.Entry.create "constr:open_binders" + let binders_fixannot = Gram.Entry.create "constr:binders_fixannot" let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint" let record_declaration = Gram.Entry.create "constr:record_declaration" let appl_arg = Gram.Entry.create "constr:appl_arg" @@ -563,10 +564,15 @@ let compute_entry allow_create adjust forpat = function else weaken_entry Constr.operconstr), adjust (n,q), false | ETName -> weaken_entry Prim.name, None, false + | ETBinder true -> anomaly "Should occur only as part of BinderList" + | ETBinder false -> weaken_entry Constr.binder, None, false + | ETBinderList (true,tkl) -> + assert (tkl=[]); weaken_entry Constr.open_binders, None, false + | ETBinderList (false,_) -> anomaly "List of entries cannot be registered." | ETBigint -> weaken_entry Prim.bigint, None, false | ETReference -> weaken_entry Constr.global, None, false | ETPattern -> weaken_entry Constr.pattern, None, false - | ETConstrList _ -> error "List of entries cannot be registered." + | ETConstrList _ -> anomaly "List of entries cannot be registered." | ETOther (u,n) -> let u = get_univ u in let e = @@ -606,6 +612,12 @@ let is_binder_level from e = ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true | _ -> false +let make_sep_rules tkl = + Gramext.srules + [List.map (fun x -> Gramext.Stoken x) tkl, + List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl + (Gramext.action (fun loc -> ()))] + let rec symbol_of_constr_prod_entry_key assoc from forpat typ = if is_binder_level from typ then if forpat then @@ -621,10 +633,14 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = | ETConstrList (typ',tkl) -> Gramext.Slist1sep (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), - Gramext.srules - [List.map (fun x -> Gramext.Stoken x) tkl, - List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl - (Gramext.action (fun loc -> ()))]) + make_sep_rules tkl) + | ETBinderList (false,[]) -> + Gramext.Slist1 + (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) + | ETBinderList (false,tkl) -> + Gramext.Slist1sep + (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), + make_sep_rules tkl) | _ -> match interp_constr_prod_entry_key assoc from forpat typ with | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 88bf9c1c..e4566e77 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: pcoq.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) open Util open Names @@ -203,10 +203,11 @@ module Constr : val pattern : cases_pattern_expr Gram.Entry.e val constr_pattern : constr_expr Gram.Entry.e val lconstr_pattern : constr_expr Gram.Entry.e - val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e - val binder_let : local_binder list Gram.Entry.e - val binders_let : local_binder list Gram.Entry.e - val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e + val closed_binder : local_binder list Gram.Entry.e + val binder : local_binder list Gram.Entry.e (* closed_binder or variable *) + val binders : local_binder list Gram.Entry.e + val open_binders : local_binder list Gram.Entry.e + val binders_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e val record_declaration : constr_expr Gram.Entry.e val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index fcdc2aee..eef28fcf 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ppconstr.ml 13358 2010-07-29 23:10:17Z herbelin $ *) (*i*) open Util @@ -64,8 +64,8 @@ let prec_of_prim_token = function open Notation -let print_hunks n pr (env,envlist) unp = - let env = ref env and envlist = ref envlist in +let print_hunks n pr pr_binders (terms,termlists,binders) unp = + let env = ref terms and envlist = ref termlists and bll = ref binders in let pop r = let a = List.hd !r in r := List.tl !r; a in let rec aux = function | [] -> mt () @@ -76,6 +76,8 @@ let print_hunks n pr (env,envlist) unp = let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in let pp2 = aux l in pp1 ++ pp2 + | UnpBinderListMetaVar (_,isopen,sl) :: l -> + let cl = pop bll in pr_binders (fun () -> aux sl) isopen cl ++ aux l | UnpTerminal s :: l -> str s ++ aux l | UnpBox (b,sub) :: l -> (* Keep order: side-effects *) @@ -85,9 +87,9 @@ let print_hunks n pr (env,envlist) unp = | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in aux unp -let pr_notation pr s env = +let pr_notation pr pr_binders s env = let unpl, level = find_notation_printing_rule s in - print_hunks level pr env unpl, level + print_hunks level pr pr_binders env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) @@ -191,7 +193,8 @@ let rec pr_patt sep inh p = hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator | CPatNotation (_,"( _ )",([p],[])) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom - | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env + | CPatNotation (_,s,(l,ll)) -> + pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) | CPatPrim (_,p) -> pr_prim_token p, latom | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 in @@ -254,18 +257,22 @@ let pr_binder_among_many pr_c = function hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) -let pr_undelimited_binders pr_c = - prlist_with_sep spc (pr_binder_among_many pr_c) +let pr_undelimited_binders sep pr_c = + prlist_with_sep sep (pr_binder_among_many pr_c) -let pr_delimited_binders kw pr_c bl = +let pr_delimited_binders kw sep pr_c bl = let n = begin_of_binders bl in match bl with | [LocalRawAssum (nal,k,t)] -> pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) | LocalRawAssum _ :: _ as bdl -> - pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl + pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl | _ -> assert false +let pr_binders_gen pr_c sep is_open = + if is_open then pr_delimited_binders mt sep pr_c + else pr_undelimited_binders sep pr_c + let rec extract_prod_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_prod_binders c in @@ -399,7 +406,7 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in pr_id id ++ str" " ++ - hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++ + hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++ pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c @@ -446,7 +453,7 @@ let tm_clash = function let pr_asin pr (na,indnalopt) = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) - | Some na -> spc () ++ str "as " ++ pr_name na + | Some na -> spc () ++ str "as " ++ pr_lname na | None -> mt ()) ++ (match indnalopt with | None -> mt () @@ -465,7 +472,7 @@ let pr_return_type pr po = pr_case_type pr po let pr_simple_return_type pr na po = (match na with - | Some (Name id) -> + | Some (_,Name id) -> spc () ++ str "as " ++ pr_id id | _ -> mt ()) ++ pr_case_type pr po @@ -483,15 +490,11 @@ let pr_app pr a l = pr (lapp,L) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) -let pr_forall () = - if !Flags.unicode_syntax then str"Π" ++ spc () - else str"forall" ++ spc () +let pr_forall () = str"forall" ++ spc () -let pr_fun () = - if !Flags.unicode_syntax then str"λ" ++ spc () - else str"fun" ++ spc () +let pr_fun () = str"fun" ++ spc () -let pr_fun_sep = lazy (if !Flags.unicode_syntax then str "," else str " =>") +let pr_fun_sep = str " =>" let pr_dangling_with_for sep pr inherited a = @@ -519,16 +522,16 @@ let pr pr sep inherited a = | CProdN _ -> let (bl,a) = extract_prod_binders a in hov 0 ( - hov 2 (pr_delimited_binders pr_forall + hov 2 (pr_delimited_binders pr_forall spc (pr mt ltop) bl) ++ str "," ++ pr spc ltop a), lprod | CLambdaN _ -> let (bl,a) = extract_lam_binders a in hov 0 ( - hov 2 (pr_delimited_binders pr_fun + hov 2 (pr_delimited_binders pr_fun spc (pr mt ltop) bl) ++ - Lazy.force pr_fun_sep ++ pr spc ltop a), + pr_fun_sep ++ pr spc ltop a), llambda | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) when x=x' -> @@ -599,7 +602,7 @@ let pr pr sep inherited a = hv 0 ( str "let " ++ hov 0 (str "(" ++ - prlist_with_sep sep_v pr_name nal ++ + prlist_with_sep sep_v pr_lname nal ++ str ")" ++ pr_simple_return_type (pr mt) na po ++ str " :=" ++ pr spc ltop c ++ str " in") ++ @@ -626,9 +629,10 @@ let pr pr sep inherited a = | CCast (_,a,CastCoerce) -> hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), lcast - | CNotation (_,"( _ )",([t],[])) -> + | CNotation (_,"( _ )",([t],[],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom - | CNotation (_,s,env) -> pr_notation (pr mt) s env + | CNotation (_,s,env) -> + pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1 @@ -700,7 +704,7 @@ let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c let pr_cases_pattern_expr = pr_patt ltop -let pr_binders = pr_undelimited_binders (pr ltop) +let pr_binders = pr_undelimited_binders spc (pr ltop) let pr_with_occurrences pr occs = match occs with diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 0d566a5d..1ad110cb 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ppconstr.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Environ diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml index b276444f..275b02df 100644 --- a/parsing/ppdecl_proof.ml +++ b/parsing/ppdecl_proof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ppdecl_proof.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Pp diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index ba7558f7..f27959c2 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: pptactic.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Names diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 46786997..bb9d8426 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: pptactic.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Genarg diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 83fcff7e..ff35be57 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ppvernac.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Names @@ -113,7 +113,9 @@ let pr_set_entry_type = function | ETConstr _ -> str"constr" | ETOther (_,e) -> str e | ETBigint -> str "bigint" - | ETConstrList _ -> failwith "Internal entry type" + | ETBinder true -> str "binder" + | ETBinder false -> str "closed binder" + | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" let strip_meta id = let s = string_of_id id in @@ -330,6 +332,14 @@ let pr_onescheme (idop,schem) = hov 0 ((if dep then str"Induction for" else str"Minimality for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) + | CaseScheme (dep,ind,s) -> + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc () + ) ++ + hov 0 ((if dep then str"Elimination for" else str"Case for") + ++ spc() ++ pr_smart_global ind) ++ spc() ++ + hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) | EqualityScheme ind -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index f1322914..dce1bbd7 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ppvernac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Genarg diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 8f12ec6d..9c39e57e 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id$ *) +(* $Id: prettyp.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 9cda516e..d7f83b63 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: prettyp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/parsing/printer.ml b/parsing/printer.ml index 54d7065c..c9f27678 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: printer.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/parsing/printer.mli b/parsing/printer.mli index 63493768..a6f73a40 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: printer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 84340cae..fff29083 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) +(* $Id: q_constr.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Rawterm open Term diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 0f2ef78b..d0afcdd4 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*) -(* $Id$ *) +(* $Id: q_coqast.ml4 13329 2010-07-26 11:05:39Z herbelin $ *) open Util open Names @@ -162,11 +162,10 @@ let rec mlexpr_of_constr = function | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >> | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" - | Topconstr.CNotation(_,ntn,subst) -> + | Topconstr.CNotation(_,ntn,(subst,substl,[])) -> <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$ - $mlexpr_of_pair - (mlexpr_of_list mlexpr_of_constr) - (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >> + ($mlexpr_of_list mlexpr_of_constr subst$, + $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >> | Topconstr.CPatVar (loc,n) -> <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> | _ -> failwith "mlexpr_of_constr: TODO" diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index a23e4b18..6d6c229c 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "q_MLast.cmo" i*) -(* $Id$ *) +(* $Id: q_util.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) (* This file defines standard combinators to build ml expressions *) diff --git a/parsing/q_util.mli b/parsing/q_util.mli index 7617dc53..c55d8482 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: q_util.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) val patt_of_expr : MLast.expr -> MLast.patt diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 465465fa..f067fcf3 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) +(* $Id: tacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Genarg diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index ff87ac03..3d048c30 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: tactic_printer.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli index 3584f626..9233233f 100644 --- a/parsing/tactic_printer.mli +++ b/parsing/tactic_printer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: tactic_printer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 05c5ef86..95eccfda 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) +(* $Id: vernacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Genarg -- cgit v1.2.3