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 --- toplevel/auto_ind_decl.ml | 2 +- toplevel/cerrors.ml | 2 +- toplevel/cerrors.mli | 2 +- toplevel/class.ml | 2 +- toplevel/class.mli | 2 +- toplevel/classes.ml | 4 +- toplevel/classes.mli | 2 +- toplevel/command.ml | 62 ++++++----- toplevel/command.mli | 14 +-- toplevel/coqinit.ml | 2 +- toplevel/coqinit.mli | 2 +- toplevel/coqtop.ml | 4 +- toplevel/coqtop.mli | 2 +- toplevel/discharge.ml | 2 +- toplevel/discharge.mli | 2 +- toplevel/himsg.ml | 4 +- toplevel/himsg.mli | 2 +- toplevel/ind_tables.ml | 2 +- toplevel/indschemes.ml | 72 ++++++------ toplevel/indschemes.mli | 2 +- toplevel/lemmas.ml | 2 +- toplevel/lemmas.mli | 2 +- toplevel/metasyntax.ml | 265 ++++++++++++++++++++++++++++++--------------- toplevel/metasyntax.mli | 4 +- toplevel/mltop.ml4 | 2 +- toplevel/mltop.mli | 2 +- toplevel/record.ml | 10 +- toplevel/record.mli | 2 +- toplevel/search.ml | 2 +- toplevel/search.mli | 2 +- toplevel/toplevel.ml | 2 +- toplevel/toplevel.mli | 2 +- toplevel/usage.ml | 2 +- toplevel/usage.mli | 2 +- toplevel/vernac.ml | 2 +- toplevel/vernac.mli | 2 +- toplevel/vernacentries.ml | 5 +- toplevel/vernacentries.mli | 2 +- toplevel/vernacexpr.ml | 3 +- toplevel/vernacinterp.ml | 2 +- toplevel/vernacinterp.mli | 2 +- toplevel/whelp.ml4 | 2 +- toplevel/whelp.mli | 2 +- 43 files changed, 303 insertions(+), 208 deletions(-) (limited to 'toplevel') diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 809af337..6064c3d4 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: auto_ind_decl.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (* This file is about the automatic generation of schemes about decidable equality, created by Vincent Siles, Oct 2007 *) diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 071731ac..5828f12d 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: cerrors.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index e2c42d50..00316007 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: cerrors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/class.ml b/toplevel/class.ml index 49b3399c..0ee9dd19 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: class.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Pp diff --git a/toplevel/class.mli b/toplevel/class.mli index 7410ed32..057d85ac 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: class.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 4c334e0b..435ddb4d 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: classes.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Names @@ -149,7 +149,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, cty, ctx', ctx, len, imps, subst = let (env', ctx), imps = interp_context_evars evars env ctx in - let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in + let c', imps' = interp_type_evars_impls ~evdref:evars ~fail_evar:false env' tclass in let len = List.length ctx in let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum c' in diff --git a/toplevel/classes.mli b/toplevel/classes.mli index a19d5dbb..61670e0d 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: classes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/command.ml b/toplevel/command.ml index 1f6e7e83..9b18ef27 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: command.ml 13344 2010-07-28 15:04:36Z msozeau $ *) open Pp open Util @@ -69,8 +69,7 @@ let red_constant_entry n ce = function let interp_definition boxed bl red_option c ctypopt = let env = Global.env() in let evdref = ref Evd.empty in - let (env_bl, ctx), imps1 = - interp_context_evars ~fail_anonymous:false evdref env bl in + let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in let imps,ce = match ctypopt with None -> @@ -227,7 +226,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = let env0 = Global.env() in let evdref = ref Evd.empty in let (env_params, ctx_params), userimpls = - interp_context_evars ~fail_anonymous:false evdref env0 paramsl + interp_context_evars evdref env0 paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -244,7 +243,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in let arities = List.map fst arities in - let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in + let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = @@ -256,9 +255,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite = () in (* Instantiate evars and check all are resolved *) - let evd,_ = consider_remaining_unif_problems env_params !evdref in + let evd = consider_remaining_unif_problems env_params !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in - let sigma = evd in + let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in @@ -448,14 +447,19 @@ let check_mutuality env isfix fixl = type structured_fixpoint_expr = { fix_name : identifier; + fix_annot : identifier located option; fix_binders : local_binder list; fix_body : constr_expr option; fix_type : constr_expr } -let interp_fix_context evdref env fix = - interp_context_evars evdref env fix.fix_binders - +let interp_fix_context evdref env isfix fix = + let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in + let (env', ctx), imps = interp_context_evars evdref env before in + let (env'', ctx'), imps' = interp_context_evars evdref env' after in + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + ((env'', ctx' @ ctx), imps @ imps', annot) + let interp_fix_ccl evdref (env,_) fix = interp_type_evars evdref env fix.fix_type @@ -487,8 +491,8 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs = (* Jump over let-bindings. *) -let compute_possible_guardness_evidences na fix (ids,_) = - match index_of_annot fix.fix_binders na with +let compute_possible_guardness_evidences (ids,_,na) = + match na with | Some i -> [i] | None -> (* If recursive argument was not given by user, we try all args. @@ -507,15 +511,15 @@ let interp_recursive isfix fixl notations = (* Interp arities allowing for unresolved types *) let evdref = ref Evd.empty in - let fixctxs, fiximps = - List.split (List.map (interp_fix_context evdref env) fixl) in + let fixctxs, fiximps, fixannots = + list_split3 (List.map (interp_fix_context evdref env isfix) fixl) in let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (nf_evar !evdref) fixtypes in let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in + let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = @@ -525,7 +529,7 @@ let interp_recursive isfix fixl notations = () in (* Instantiate evars and check all are resolved *) - let evd,_ = consider_remaining_unif_problems env_rec !evdref in + let evd = consider_remaining_unif_problems env_rec !evdref in let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in let fixtypes = List.map (nf_evar evd) fixtypes in let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in @@ -538,7 +542,7 @@ let interp_recursive isfix fixl notations = end; (* Build the fix declaration block *) - (fixnames,fixdefs,fixtypes),List.combine fixctxnames fiximps + (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots let interp_fixpoint = interp_recursive true let interp_cofixpoint = interp_recursive false @@ -547,7 +551,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) let thms = - list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in + list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -558,7 +562,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in - let fiximps = List.map snd fiximps in + let fiximps = List.map (fun (n,r,p) -> r) fiximps in let fixdecls = list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps); @@ -572,7 +576,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) let thms = - list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in + list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -583,7 +587,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let fiximps = List.map snd fiximps in + let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames @@ -592,28 +596,28 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = List.iter Metasyntax.add_notation_interpretation ntns let extract_decreasing_argument = function - | (_,(na,CStructRec),_,_,_) -> na + | (na,CStructRec) -> na | _ -> error "Only structural decreasing is supported for a non-Program Fixpoint" let extract_fixpoint_components l = let fixl, ntnl = List.split l in - let wfl = List.map extract_decreasing_argument fixl in - let fixl = List.map (fun ((_,id),_,bl,typ,def) -> - {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in - fixl, List.flatten ntnl, wfl + let fixl = List.map (fun ((_,id),ann,bl,typ,def) -> + let ann = extract_decreasing_argument ann in + {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in + fixl, List.flatten ntnl let extract_cofixpoint_components l = let fixl, ntnl = List.split l in List.map (fun ((_,id),bl,typ,def) -> - {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, + {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl let do_fixpoint l b = - let fixl,ntns,wfl = extract_fixpoint_components l in + let fixl,ntns = extract_fixpoint_components l in let fix = interp_fixpoint fixl ntns in let possible_indexes = - list_map3 compute_possible_guardness_evidences wfl fixl (snd fix) in + List.map compute_possible_guardness_evidences (snd fix) in declare_fixpoint b fix possible_indexes ntns let do_cofixpoint l b = diff --git a/toplevel/command.mli b/toplevel/command.mli index ab94e7d2..f5996905 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: command.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Util @@ -102,6 +102,7 @@ val do_mutual_inductive : type structured_fixpoint_expr = { fix_name : identifier; + fix_annot : identifier located option; fix_binders : local_binder list; fix_body : constr_expr option; fix_type : constr_expr @@ -112,8 +113,7 @@ type structured_fixpoint_expr = { val extract_fixpoint_components : (fixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list * - (* possible structural arg: *) lident option list + structured_fixpoint_expr list * decl_notation list val extract_cofixpoint_components : (cofixpoint_expr * decl_notation list) list -> @@ -126,20 +126,20 @@ type recursive_preentry = val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * manual_implicits) list + recursive_preentry * (name list * manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * manual_implicits) list + recursive_preentry * (name list * manual_implicits * int option) list (* Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - bool -> recursive_preentry * (name list * manual_implicits) list -> + bool -> recursive_preentry * (name list * manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : - bool -> recursive_preentry * (name list * manual_implicits) list -> + bool -> recursive_preentry * (name list * manual_implicits * int option) list -> decl_notation list -> unit (* Entry points for the vernacular commands Fixpoint and CoFixpoint *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 5f9f96a9..bce38128 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: coqinit.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open System diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 926ecf8f..c2a535dd 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: coqinit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Initialization. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 3d3010dd..f05509a4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: coqtop.ml 13358 2010-07-29 23:10:17Z herbelin $ *) open Pp open Util @@ -281,7 +281,7 @@ let parse_args is_ide = | "-emacs-U" :: rem -> Flags.print_emacs := true; Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem - | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem + | "-unicode" :: rem -> add_require "Utf8_core"; parse rem | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem | "-coqlib" :: [] -> usage () diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index f5e3a464..e80b3252 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: coqtop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* The Coq main module. The following function [start] will parse the command line, print the banner, initialize the load path, load the input diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index af02253b..6f74c526 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: discharge.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Names open Util diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index a2cbb6be..dda4c5d7 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: discharge.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Sign open Cooking diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a97bf9bb..a080442c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: himsg.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -543,7 +543,7 @@ let explain_unsatisfiable_constraints env evd constr = match constr with | None -> str"Unable to satisfy the following constraints:" ++ fnl() ++ - pr_constraints true env evm + pr_constraints true env undef | Some (ev, k) -> explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++ if List.length (Evd.to_list undef) > 1 then diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 856583d9..a916e87b 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: himsg.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 6f692ced..4e28ccac 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ind_tables.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (* File created by Vincent Siles, Oct 2007, extended into a generic support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index ef3efa47..29d7a12c 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: indschemes.ml 13333 2010-07-27 10:18:30Z vsiles $ *) (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent @@ -54,7 +54,7 @@ let _ = optread = (fun () -> !elim_flag) ; optwrite = (fun b -> elim_flag := b) } -let case_flag = ref true +let case_flag = ref false let _ = declare_bool_option { optsync = true; @@ -63,7 +63,7 @@ let _ = optread = (fun () -> !case_flag) ; optwrite = (fun b -> case_flag := b) } -let eq_flag = ref true +let eq_flag = ref false let _ = declare_bool_option { optsync = true; @@ -292,6 +292,7 @@ let rec split_scheme l = | (Some id,t)::q -> let l1,l2 = split_scheme q in ( match t with | InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2 + | CaseScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2 | EqualityScheme x -> l1,((Some id,smart_global_inductive x)::l2) ) (* @@ -299,38 +300,41 @@ let rec split_scheme l = requested *) | (None,t)::q -> - let l1,l2 = split_scheme q in - ( match t with - | InductionScheme (x,y,z) -> - let ind = smart_global_inductive y in - let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in - let z' = family_of_sort (interp_sort z) in - let suffix = ( - match sort_of_ind with - | InProp -> - if x then (match z' with - | InProp -> "_ind_nodep" - | InSet -> "_rec_nodep" - | InType -> "_rect_nodep") - else ( match z' with - | InProp -> "_ind" - | InSet -> "_rec" - | InType -> "_rect" ) - | _ -> - if x then (match z' with - | InProp -> "_ind" - | InSet -> "_rec" - | InType -> "_rect" ) - else (match z' with - | InProp -> "_ind_dep" - | InSet -> "_rec_dep" - | InType -> "_rect_dep") - ) in - let newid = add_suffix (basename_of_global (IndRef ind)) suffix in - let newref = (dummy_loc,newid) in + let l1,l2 = split_scheme q in + let names inds recs x y z = + let ind = smart_global_inductive y in + let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in + let z' = family_of_sort (interp_sort z) in + let suffix = ( + match sort_of_ind with + | InProp -> + if x then (match z' with + | InProp -> inds ^ "_nodep" + | InSet -> recs ^ "_nodep" + | InType -> recs ^ "t_nodep") + else ( match z' with + | InProp -> inds + | InSet -> recs + | InType -> recs ^ "t" ) + | _ -> + if x then (match z' with + | InProp -> inds + | InSet -> recs + | InType -> recs ^ "t" ) + else (match z' with + | InProp -> inds ^ "_dep" + | InSet -> recs ^ "_dep" + | InType -> recs ^ "t_dep") + ) in + let newid = add_suffix (basename_of_global (IndRef ind)) suffix in + let newref = (dummy_loc,newid) in ((newref,x,ind,z)::l1),l2 - | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2) - ) + in + match t with + | CaseScheme (x,y,z) -> names "_case" "_case" x y z + | InductionScheme (x,y,z) -> names "_ind" "_rec" x y z + | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2) + let do_mutual_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index 76a5e4b7..f763e182 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: indschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 89252e54..7af5d0aa 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: lemmas.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index e0700341..5327f63f 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: lemmas.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a297d1d7..6ee00f48 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: metasyntax.ml 13329 2010-07-26 11:05:39Z herbelin $ *) open Pp open Flags @@ -280,7 +280,7 @@ let rec find_pattern nt xl = function | [], NonTerminal x' :: l' -> (out_nt nt,x',List.rev xl),l' | [], Terminal s :: _ | Terminal s :: _, _ -> - error ("The token "^s^" occurs on one side of \"..\" but not on the other side.") + error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.") | [], Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | _, [] -> @@ -289,23 +289,23 @@ let rec find_pattern nt xl = function anomaly "Only Terminal or Break expected on left, non-SProdList on right" let rec interp_list_parser hd = function - | [] -> [], [], List.rev hd + | [] -> [], List.rev hd | NonTerminal id :: tl when id = ldots_var -> let hd = List.rev hd in let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in - let yl,xl,tl'' = interp_list_parser [] tl' in + let xyl,tl'' = interp_list_parser [] tl' in (* We remember each pair of variable denoting a recursive part to *) (* remove the second copy of it afterwards *) - (y,x)::yl, x::xl, SProdList (x,sl) :: tl'' + (x,y)::xyl, SProdList (x,sl) :: tl'' | (Terminal _ | Break _) as s :: tl -> if hd = [] then - let yl,xl,tl' = interp_list_parser [] tl in - yl, xl, s :: tl' + let yl,tl' = interp_list_parser [] tl in + yl, s :: tl' else interp_list_parser (s::hd) tl | NonTerminal _ as x :: tl -> - let yl,xl,tl' = interp_list_parser [x] tl in - yl, xl, List.rev_append hd tl' + let xyl,tl' = interp_list_parser [x] tl in + xyl, List.rev_append hd tl' | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" @@ -345,33 +345,28 @@ let rec get_notation_vars = function | [] -> [] | NonTerminal id :: sl -> let vars = get_notation_vars sl in - if List.mem id vars then - if id <> ldots_var then + if id = ldots_var then vars else + if List.mem id vars then error ("Variable "^string_of_id id^" occurs more than once.") - else - vars - else - id::vars + else + id::vars | (Terminal _ | Break _) :: sl -> get_notation_vars sl | SProdList _ :: _ -> assert false let analyze_notation_tokens l = let l = raw_analyze_notation_tokens l in let vars = get_notation_vars l in - let extrarecvars,recvars,l = interp_list_parser [] l in - (if extrarecvars = [] then [], [], vars, l - else extrarecvars, recvars, list_subtract vars recvars, l) - -let remove_extravars extrarecvars (vars,recvars) = - let vars = - List.fold_right (fun (x,y) l -> - if List.assoc x l <> List.assoc y recvars then - error - "Two end variables of a recursive notation are not in the same scope." - else - List.remove_assoc x l) - extrarecvars (List.remove_assoc ldots_var vars) in - (vars,recvars) + let recvars,l = interp_list_parser [] l in + recvars, list_subtract vars (List.map snd recvars), l + +let error_not_same_scope x y = + error ("Variables "^string_of_id x^" and "^string_of_id y^ + " must be in the same scope.") + +let error_both_bound_and_binding x y = + errorlabstrm "" (strbrk "The recursive variables " ++ pr_id x ++ + strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder + for both terms and binders.") (**********************************************************************) (* Build pretty-printing rules *) @@ -434,6 +429,13 @@ let rec is_non_terminal = function let add_break n l = UnpCut (PpBrk(n,0)) :: l +let check_open_binder isopen sl m = + if isopen & sl <> [] then + errorlabstrm "" (str "as " ++ pr_id m ++ + str " is a non-closed binder, no such \"" ++ + prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl + ++ strbrk "\" is allowed to occur.") + (* Heuristics for building default printing rules *) type previous_prod_status = NoBreak | CanBreak @@ -478,7 +480,7 @@ let make_hunks etyps symbols from = | Terminal s :: prods -> if is_right_bracket s then - UnpTerminal s ::make NoBreak prods + UnpTerminal s :: make NoBreak prods else if ws = CanBreak then add_break 1 (UnpTerminal s :: make NoBreak prods) else @@ -489,14 +491,20 @@ let make_hunks etyps symbols from = | SProdList (m,sl) :: prods -> let i = list_index m vars in - let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in + let typ = List.nth typs (i-1) in + let _,prec = precedence_of_entry_type from typ in let sl' = (* If no separator: add a break *) if sl = [] then add_break 1 [] (* We add NonTerminal for simulation but remove it afterwards *) - else snd (list_sep_last (make NoBreak (sl@[NonTerminal m]))) - in - UnpListMetaVar (i,prec,sl') :: make CanBreak prods + else snd (list_sep_last (make NoBreak (sl@[NonTerminal m]))) in + let hunk = match typ with + | ETConstr _ -> UnpListMetaVar (i,prec,sl') + | ETBinder isopen -> + check_open_binder isopen sl m; + UnpBinderListMetaVar (i,isopen,sl') + | _ -> assert false in + hunk :: make CanBreak prods | [] -> [] @@ -559,12 +567,19 @@ let hunks_of_format (from,(vars,typs)) symfmt = let symbs, l = aux (symbs,fmt) in symbs, u :: l | SProdList (m,sl) :: symbs, fmt -> let i = list_index m vars in - let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in + let typ = List.nth typs (i-1) in + let _,prec = precedence_of_entry_type from typ in let slfmt,fmt = read_recursive_format sl fmt in let sl, slfmt = aux (sl,slfmt) in if sl <> [] then error_format (); let symbs, l = aux (symbs,fmt) in - symbs, UnpListMetaVar (i,prec,slfmt) :: l + let hunk = match typ with + | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) + | ETBinder isopen -> + check_open_binder isopen sl m; + UnpBinderListMetaVar (i,isopen,slfmt) + | _ -> assert false in + symbs, hunk :: l | symbs, [] -> symbs, [] | _, _ -> error_format () in @@ -632,11 +647,13 @@ let make_production etyps symbols = (List.map (function Terminal s -> [terminal s] | Break _ -> [] | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in - let typ = match List.assoc x etyps with - | ETConstr x -> x - | _ -> - error "Component of recursive patterns in notation must be constr." in - expand_list_rule typ tkl x 1 0 [] ll) + match List.assoc x etyps with + | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll + | ETBinder o -> + distribute + [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll + | _ -> + error "Components of recursive patterns in notation must be terms or binders.") symbols [[]] in List.map define_keywords prod @@ -682,7 +699,7 @@ let error_incompatible_level ntn oldprec prec = spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") -let cache_one_syntax_extension (prec,ntn,gr,pp) = +let cache_one_syntax_extension (typs,prec,ntn,gr,pp) = try let oldprec = Notation.level_of_notation ntn in if prec <> oldprec then error_incompatible_level ntn oldprec prec @@ -690,7 +707,7 @@ let cache_one_syntax_extension (prec,ntn,gr,pp) = (* Reserve the notation level *) Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - Egrammar.extend_grammar (Egrammar.Notation (prec,gr)); + Egrammar.extend_grammar (Egrammar.Notation (prec,typs,gr)); (* Declare the printing rule *) Notation.declare_notation_printing_rule ntn (pp,fst prec) @@ -702,8 +719,9 @@ let subst_parsing_rule subst x = x let subst_printing_rule subst x = x let subst_syntax_extension (subst,(local,sy)) = - (local, List.map (fun (prec,ntn,gr,pp) -> - (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy) + (local, List.map (fun (typs,prec,ntn,gr,pp) -> + (typs,prec,ntn,subst_parsing_rule subst gr,subst_printing_rule subst pp)) + sy) let classify_syntax_definition (local,_ as o) = if local then Dispose else Substitute o @@ -768,11 +786,59 @@ let set_entry_type etyps (x,typ) = | ETConstr (n,()), (_,BorderProd (left,_)) -> ETConstr (n,BorderProd (left,None)) | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd) - | (ETPattern | ETName | ETBigint | ETOther _ | ETReference as t), _ -> t - | (ETConstrList _, _) -> assert false + | (ETPattern | ETName | ETBigint | ETOther _ | + ETReference | ETBinder _ as t), _ -> t + | (ETBinderList _ |ETConstrList _), _ -> assert false with Not_found -> ETConstr typ in (x,typ) +let join_auxiliary_recursive_types recvars etyps = + List.fold_right (fun (x,y) typs -> + let xtyp = try Some (List.assoc x etyps) with Not_found -> None in + let ytyp = try Some (List.assoc y etyps) with Not_found -> None in + match xtyp,ytyp with + | None, None -> typs + | Some _, None -> typs + | None, Some ytyp -> (x,ytyp)::typs + | Some xtyp, Some ytyp when xtyp = ytyp -> typs + | Some xtyp, Some ytyp -> + errorlabstrm "" + (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++ + strbrk ", both ends have incompatible types.")) + recvars etyps + +let internalization_type_of_entry_type = function + | ETConstr _ -> NtnInternTypeConstr + | ETBigint | ETReference -> NtnInternTypeConstr + | ETBinder _ -> NtnInternTypeBinder + | ETName -> NtnInternTypeIdent + | ETPattern | ETOther _ -> error "Not supported." + | ETBinderList _ | ETConstrList _ -> assert false + +let set_internalization_type typs = + List.map (down_snd internalization_type_of_entry_type) typs + +let make_internalization_vars recvars mainvars typs = + let maintyps = List.combine mainvars typs in + let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in + maintyps@extratyps + +let make_interpretation_type isrec = function + | NtnInternTypeConstr when isrec -> NtnTypeConstrList + | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr + | NtnInternTypeBinder when isrec -> NtnTypeBinderList + | NtnInternTypeBinder -> error "Type not allowed in recursive notation." + +let make_interpretation_vars recvars allvars = + List.iter (fun (x,y) -> + if fst (List.assoc x allvars) <> fst (List.assoc y allvars) then + error_not_same_scope x y) recvars; + let useless_recvars = List.map snd recvars in + let mainvars = + List.filter (fun (x,_) -> not (List.mem x useless_recvars)) allvars in + List.map (fun (x,(sc,typ)) -> + (x,(sc,make_interpretation_type (List.mem_assoc x recvars) typ))) mainvars + let check_rule_productivity l = if List.for_all (function NonTerminal _ -> true | _ -> false) l then error "A notation must include at least one symbol."; @@ -791,29 +857,31 @@ let find_precedence lev etyps symbols = error "The level of the leftmost non-terminal cannot be changed." | ETName | ETBigint | ETReference -> if lev = None then - if_verbose msgnl (str "Setting notation at level 0.") + ([msgnl,str "Setting notation at level 0."],0) else if lev <> Some 0 then - error "A notation starting with an atomic expression must be at level 0."; - 0 - | ETPattern | ETOther _ -> (* Give a default ? *) + error "A notation starting with an atomic expression must be at level 0." + else + ([],0) + | ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *) if lev = None then error "Need an explicit level." - else Option.get lev - | ETConstrList _ -> assert false (* internally used in grammar only *) + else [],Option.get lev + | ETConstrList _ | ETBinderList _ -> + assert false (* internally used in grammar only *) with Not_found -> if lev = None then error "A left-recursive notation must have an explicit level." - else Option.get lev) + else [],Option.get lev) | Terminal _ ::l when (match list_last symbols with Terminal _ -> true |_ -> false) -> if lev = None then - (if_verbose msgnl (str "Setting notation at level 0."); 0) - else Option.get lev + ([msgnl,str "Setting notation at level 0."], 0) + else [],Option.get lev | _ -> if lev = None then error "Cannot determine the level."; - Option.get lev + [],Option.get lev let check_curly_brackets_notation_exists () = try let _ = Notation.level_of_notation "{ _ }" in () @@ -849,13 +917,13 @@ let compute_syntax_data (df,modifiers) = (* Notation defaults to NONA *) let assoc = match assoc with None -> Some Gramext.NonA | a -> a in let toks = split_notation_string df in - let (extrarecvars,recvars,vars,symbols) = analyze_notation_tokens toks in + let (recvars,mainvars,symbols) = analyze_notation_tokens toks in let ntn_for_interp = make_notation_key symbols in let symbols' = remove_curly_brackets symbols in let need_squash = (symbols <> symbols') in let ntn_for_grammar = make_notation_key symbols' in check_rule_productivity symbols'; - let n = find_precedence n etyps symbols' in + let msgs,n = find_precedence n etyps symbols' in let innerlevel = NumLevel 200 in let typs = find_symbols @@ -864,12 +932,25 @@ let compute_syntax_data (df,modifiers) = (NumLevel n,BorderProd(Right,assoc)) symbols' in (* To globalize... *) - let typs = List.map (set_entry_type etyps) typs in - let prec = (n,List.map (assoc_of_type n) typs) in - let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in + let etyps = join_auxiliary_recursive_types recvars etyps in + let sy_typs = List.map (set_entry_type etyps) typs in + let prec = (n,List.map (assoc_of_type n) sy_typs) in + let i_typs = set_internalization_type sy_typs in + let sy_data = (n,sy_typs,symbols',fmt) in + let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in - let i_data = (onlyparse,extrarecvars,recvars,vars,(ntn_for_interp,df')) in - (i_data,sy_data) + let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in + (* Return relevant data for interpretation and for parsing/printing *) + (msgs,i_data,i_typs,sy_fulldata) + +let compute_pure_syntax_data (df,mods) = + let (msgs,(onlyparse,_,_,_),_,sy_data) = compute_syntax_data (df,mods) in + let msgs = + if onlyparse then + (msg_warning, + str "The only parsing modifier has no effect in Reserved Notation.")::msgs + else msgs in + msgs, sy_data (**********************************************************************) (* Registration of notations interpretation *) @@ -925,9 +1006,9 @@ exception NoSyntaxRule let recover_syntax ntn = try let prec = Notation.level_of_notation ntn in - let pprule,_ = Notation.find_notation_printing_rule ntn in - let gr = Egrammar.recover_notation_grammar ntn prec in - (prec,ntn,gr,pprule) + let pp_rule,_ = Notation.find_notation_printing_rule ntn in + let typs,pa_rule = Egrammar.recover_notation_grammar ntn prec in + (typs,prec,ntn,pa_rule,pp_rule) with Not_found -> raise NoSyntaxRule @@ -935,9 +1016,9 @@ let recover_squash_syntax () = recover_syntax "{ _ }" let recover_notation_syntax rawntn = let ntn = contract_notation rawntn in - let sy_rule = recover_syntax ntn in + let (typs,_,_,_,_ as sy_rule) = recover_syntax ntn in let need_squash = ntn<>rawntn in - if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule] + typs,if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule] (**********************************************************************) (* Main entry point for building parsing and printing rules *) @@ -952,10 +1033,10 @@ let make_pp_rule (n,typs,symbols,fmt) = | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] | Some fmt -> hunks_of_format (n,List.split typs) (symbols,parse_format fmt) -let make_syntax_rules (ntn,prec,need_squash,sy_data) = +let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) = let pa_rule = make_pa_rule sy_data ntn in let pp_rule = make_pp_rule sy_data in - let sy_rule = (prec,ntn,pa_rule,pp_rule) in + let sy_rule = (i_typs,prec,ntn,pa_rule,pp_rule) in (* By construction, the rule for "{ _ }" is declared, but we need to redeclare it because the file where it is declared needs not be open when the current file opens (especially in presence of -nois) *) @@ -965,31 +1046,35 @@ let make_syntax_rules (ntn,prec,need_squash,sy_data) = (* Main functions about notations *) let add_notation_in_scope local df c mods scope = - let (i_data,sy_data) = compute_syntax_data (df,mods) in - (* Declare the parsing and printing rules *) + let (msgs,i_data,i_typs,sy_data) = compute_syntax_data (df,mods) in + (* Prepare the parsing and printing rules *) let sy_rules = make_syntax_rules sy_data in - Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)); - (* Declare interpretation *) - let (onlyparse,extrarecvars,recvars,vars,df') = i_data in - let (acvars,ac) = interp_aconstr (vars,recvars) c in - let a = (remove_extravars extrarecvars acvars,ac) in + (* Prepare the interpretation *) + let (onlyparse,recvars,mainvars,df') = i_data in + let i_vars = make_internalization_vars recvars mainvars i_typs in + let (acvars,ac) = interp_aconstr i_vars recvars c in + let a = (make_interpretation_vars recvars acvars,ac) in let onlyparse = onlyparse or is_not_printable ac in + (* Ready to change the global state *) + Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; + Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)); Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df')); df' let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse = let dfs = split_notation_string df in - let (extrarecvars,recvars,vars,symbs) = analyze_notation_tokens dfs in - (* Redeclare pa/pp rules *) - if not (is_numeral symbs) then begin - let sy_rules = recover_notation_syntax (make_notation_key symbs) in - Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) - end; + let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in + (* Recover types of variables and pa/pp rules; redeclare them if needed *) + let i_typs = if not (is_numeral symbs) then begin + let i_typs,sy_rules = recover_notation_syntax (make_notation_key symbs) in + Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)); i_typs + end else [] in (* Declare interpretation *) let path = (Lib.library_dp(),Lib.current_dirpath true) in let df' = (make_notation_key symbs,(path,df)) in - let (acvars,ac) = interp_aconstr ~impls (vars,recvars) c in - let a = (remove_extravars extrarecvars acvars,ac) in + let i_vars = make_internalization_vars recvars mainvars i_typs in + let (acvars,ac) = interp_aconstr ~impls i_vars recvars c in + let a = (make_interpretation_vars recvars acvars,ac) in let onlyparse = onlyparse or is_not_printable ac in Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df')); df' @@ -997,8 +1082,9 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) (* Notations without interpretation (Reserved Notation) *) let add_syntax_extension local ((loc,df),mods) = - let (_,sy_data) = compute_syntax_data (df,mods) in + let msgs,sy_data = compute_pure_syntax_data (df,mods) in let sy_rules = make_syntax_rules sy_data in + Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) (* Notations with only interpretation *) @@ -1090,7 +1176,10 @@ let try_interp_name_alias = function let add_syntactic_definition ident (vars,c) local onlyparse = let vars,pat = try [], ARef (try_interp_name_alias (vars,c)) - with Not_found -> let (vars,_),pat = interp_aconstr (vars,[]) c in vars,pat + with Not_found -> + let i_vars = List.map (fun id -> (id,NtnInternTypeConstr)) vars in + let vars,pat = interp_aconstr i_vars [] c in + List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat in let onlyparse = onlyparse or is_not_printable pat in Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 2fd7749d..d8dd0d52 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: metasyntax.mli 13328 2010-07-26 11:05:30Z herbelin $ i*) (*i*) open Util @@ -47,7 +47,7 @@ val add_notation_interpretation : (* Add a notation interpretation for supporting the "where" clause *) -val set_notation_for_interpretation : Constrintern.full_internalization_env -> +val set_notation_for_interpretation : Constrintern.internalization_env -> (lstring * constr_expr * scope_name option) -> unit (* Add only the parsing/printing rule of a notation *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 5cefe263..e8c06d13 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -11,7 +11,7 @@ * camlp4deps will not work for this file unless Makefile system enhanced. *) -(* $Id$ *) +(* $Id: mltop.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Pp diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index c2d65493..12b6f78f 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: mltop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* If there is a toplevel under Coq, it is described by the following record. *) diff --git a/toplevel/record.ml b/toplevel/record.ml index ae53b0cf..cd569178 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: record.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -32,7 +32,6 @@ open Topconstr (********** definition d'un record (structure) **************) let interp_evars evdref env impls k typ = - let impls = set_internalization_env_params impls [] in let typ' = intern_gen true ~impls !evdref env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env k typ' @@ -48,8 +47,7 @@ let interp_fields_evars evars env nots l = | Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls in let d = (i,b',t') in - let impls' = set_internalization_env_params impls [] in - List.iter (Metasyntax.set_notation_for_interpretation impls') no; + List.iter (Metasyntax.set_notation_for_interpretation impls) no; (push_rel d env, impl :: uimpls, d::params, impls)) (env, [], [], []) nots l @@ -62,13 +60,13 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields id t ps nots fs = let env0 = Global.env () in let evars = ref Evd.empty in - let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in + let (env1,newps), imps = interp_context_evars evars env0 ps in let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let env2,impls,newfs,data = interp_fields_evars evars env_ar nots (binders_of_decls fs) in - let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in + let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in let evars = Typeclasses.resolve_typeclasses env_ar evars in let sigma = evars in let newps = Evarutil.nf_rel_context_evar sigma newps in diff --git a/toplevel/record.mli b/toplevel/record.mli index eae279f3..ea4a3b7e 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: record.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/search.ml b/toplevel/search.ml index a358f687..0bd552af 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: search.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/toplevel/search.mli b/toplevel/search.mli index b4b971a7..a73052f2 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: search.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Names diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 64096152..9594c988 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: toplevel.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index 92c8ddc4..a614c1da 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: toplevel.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/toplevel/usage.ml b/toplevel/usage.ml index dcee9921..22588f2c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: usage.ml 13323 2010-07-24 15:57:30Z herbelin $ *) let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 662f56ad..1167750b 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: usage.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s Prints the version number on the standard output and exits (with 0). *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 17792579..7f8bcb9e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: vernac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* Parsing of vernacular. *) diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index d925614c..dc4d9e2f 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: vernac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Parsing of vernacular. *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3a5e1da8..254f690c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: vernacentries.ml 13329 2010-07-26 11:05:39Z herbelin $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -626,7 +626,6 @@ let vernac_instance abst glob sup inst props pri = ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri) let vernac_context l = - List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l; Classes.context l let vernac_declare_instance glob id = @@ -1079,7 +1078,7 @@ let vernac_global_check c = let vernac_print = function | PrintTables -> print_tables () - | PrintFullContext -> msg (print_full_context_typ ()) + | PrintFullContext-> msg (print_full_context_typ ()) | PrintSectionContext qid -> msg (print_sec_context_typ qid) | PrintInspect n -> msg (inspect n) | PrintGrammar ent -> Metasyntax.print_grammar ent diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 031864fd..10ed35a7 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: vernacentries.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 1f3261e1..5eb220cb 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: vernacexpr.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) open Util open Names @@ -197,6 +197,7 @@ type proof_end = type scheme = | InductionScheme of bool * reference or_by_notation * sort_expr + | CaseScheme of bool * reference or_by_notation * sort_expr | EqualityScheme of reference or_by_notation type vernac_expr = diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 90d8d9dd..f3d2e7a5 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: vernacinterp.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 8bcbe5f3..ce64188c 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: vernacinterp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Tacexpr diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 20928cbe..15caaddd 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: whelp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Flags open Pp diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli index d6beeca1..27c36239 100644 --- a/toplevel/whelp.mli +++ b/toplevel/whelp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: whelp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Coq interface to the Whelp query engine developed at the University of Bologna *) -- cgit v1.2.3