diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | contrib/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.ml | 13 | ||||
| -rw-r--r-- | interp/constrintern.mli | 4 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 2 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 6 | ||||
| -rw-r--r-- | toplevel/classes.ml | 8 | ||||
| -rw-r--r-- | toplevel/command.ml | 8 | ||||
| -rw-r--r-- | toplevel/command.mli | 5 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
11 files changed, 37 insertions, 19 deletions
@@ -435,6 +435,10 @@ Tools - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir". - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R. - The binary "parser" has been renamed to "coq-parser". +- Improved coqdoc and dump of globalization information to give more meta-information + on identifiers. All categories of Coq definitions are supported, which makes + typesetting trivial in the generated documentation. Support for hyperlinking + and indexing developments in the tex output has been implemented as well. Miscellaneous diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 79ef009729..027aae7a79 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -168,7 +168,7 @@ let build_newrecursive if Impargs.is_implicit_args() then Impargs.compute_implicits env0 arity else [] in - let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in + let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in (Environ.push_named (recname,None,arity) env, impls')) (env0,[]) lnameargsardef in let recdef = diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 503f346193..1914002124 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -385,7 +385,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) - let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in + let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index be7c75663b..15c816b5b4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -26,8 +26,10 @@ open Inductiveops (* To interpret implicits and arg scopes of recursive variables in inductive types and recursive definitions *) +type var_internalisation_type = Inductive | Recursive | Method + type var_internalisation_data = - identifier list * Impargs.implicits_list * scope_name option list + var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list type implicits_env = (identifier * var_internalisation_data) list type full_implicits_env = identifier list * implicits_env @@ -279,13 +281,20 @@ let rec it_mkRLambda env body = [vars2] is the set of global variables, env is the set of variables abstracted until this point *) +let string_of_ty = function + | Inductive -> "ind" + | Recursive -> "def" + | Method -> "meth" + let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id = let (vars1,unbndltacvars) = ltacvars in (* Is [id] an inductive type potentially with implicit *) try - let l,impl,argsc = List.assoc id impls in + let ty, l,impl,argsc = List.assoc id impls in let l = List.map (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in + let tys = string_of_ty ty in + Dumpglob.dump_reference loc "<>" (string_of_id id) tys; RVar (loc,id), impl, argsc, l with Not_found -> (* Is [id] bound in current env or is an ltac var bound to constr *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 27a46daf19..9169e5fbf1 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -39,8 +39,10 @@ open Pretyping argument associates a list of implicit positions and scopes to identifiers declared in the [rel_context] of [env] *) +type var_internalisation_type = Inductive | Recursive | Method + type var_internalisation_data = - identifier list * Impargs.implicits_list * scope_name option list + var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list type implicits_env = (identifier * var_internalisation_data) list type full_implicits_env = identifier list * implicits_env diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index c1d7f34cee..7c7362cade 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -284,7 +284,7 @@ Definition predicate_implication {l : list Type} := (** Notations for pointwise equivalence and implication of predicates. *) Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. -Infix "-∙>" := predicate_implication (at level 70) : predicate_scope. +Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. Open Local Scope predicate_scope. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 11f710997e..d299d9dda6 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Program.Equality"); compile-command: "make -C ../.. TIME='time'" -*- *) +(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -498,12 +498,13 @@ Ltac equations := set_eos ; | _ => nonrec_equations end. +(* Equations NoConfusion_nat (P : Prop) (x y : nat) : Prop := NoConfusion_nat P 0 0 := P -> P ; NoConfusion_nat P 0 (S y) := P ; NoConfusion_nat P (S x) 0 := P ; NoConfusion_nat P (S x) (S y) := (x = y -> P) -> P. -Debug Off. + Solve Obligations using equations. Equations noConfusion_nat (P : Prop) (x y : nat) (H : x = y) : NoConfusion_nat P x y := @@ -569,3 +570,4 @@ noConfusion_list P A (cons a x) (cons a x) refl := λ p : a = a -> x = x -> P, p Instance list_noconf A : NoConfusionPackage (list A) := NoConfusion := λ P, Π x y, x = y -> NoConfusion_list P A x y ; noConfusion := λ P x y, noConfusion_list P A x y. +*)
\ No newline at end of file diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 8dcbf4b282..bf9ee12695 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -99,7 +99,7 @@ let interp_type_evars evdref env ?(impls=([],[])) typ = let mk_interning_data env na impls typ = let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (na, ([], impl, Notation.compute_arguments_scope typ)) + in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) let interp_fields_evars isevars env avoid l = List.fold_left @@ -160,8 +160,8 @@ let new_class id par ar sup props = let supnames = List.fold_left (fun acc b -> match b with - LocalRawAssum (nl, _, _) -> nl @ acc - | LocalRawDef _ -> assert(false)) + | LocalRawAssum (nl, _, _) -> nl @ acc + | LocalRawDef _ -> assert(false)) [] sup in @@ -241,7 +241,7 @@ let new_class id par ar sup props = params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) in IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y) - fields (Recordops.lookup_projections (kn,0))) + (List.rev fields) (Recordops.lookup_projections (kn,0))) in let ctx_context = List.map (fun ((na, b, t) as d) -> diff --git a/toplevel/command.ml b/toplevel/command.ml index f18cecb207..9ae3f8e826 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -442,7 +442,7 @@ let declare_eliminations sp = (* 3b| Mutual inductive definitions *) -let compute_interning_datas env l nal typl impll = +let compute_interning_datas env ty l nal typl impll = let mk_interning_data na typ impls = let idl, impl = let impl = @@ -452,7 +452,7 @@ let compute_interning_datas env l nal typl impll = let sub_impl' = List.filter is_status_implicit sub_impl in (List.map name_of_implicit sub_impl', impl) in - (na, (idl, impl, compute_arguments_scope typ)) in + (na, (ty, idl, impl, compute_arguments_scope typ)) in (l, list_map3 mk_interning_data nal typl impll) let declare_interning_data (_,impls) (df,c,scope) = @@ -526,7 +526,7 @@ let interp_mutual paramsl indl notations finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun _ -> userimpls) fullarities in - let impls = compute_interning_datas env0 params indnames fullarities indimpls in + let impls = compute_interning_datas env0 Inductive params indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = @@ -832,7 +832,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_interning_datas env [] fixnames fixtypes fiximps in + let impls = compute_interning_datas env Recursive [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) diff --git a/toplevel/command.mli b/toplevel/command.mli index 227152f14f..a1e976c792 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -56,10 +56,11 @@ val declare_assumption : identifier located list -> val declare_interning_data : 'a * Constrintern.implicits_env -> string * Topconstr.constr_expr * Topconstr.scope_name option -> unit -val compute_interning_datas : Environ.env -> 'a list -> 'b list -> +val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type -> + 'a list -> 'b list -> Term.types list ->Impargs.manual_explicitation list list -> 'a list * - ('b * (Names.identifier list * Impargs.implicits_list * + ('b * (Constrintern.var_internalisation_type * Names.identifier list * Impargs.implicits_list * Topconstr.scope_name option list)) list diff --git a/toplevel/record.ml b/toplevel/record.ml index b1271f5162..ae97a8db4a 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -38,7 +38,7 @@ let interp_evars evdref env ?(impls=([],[])) k typ = let mk_interning_data env na impls typ = let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (out_name na, ([], impl, Notation.compute_arguments_scope typ)) + in (out_name na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) let interp_fields_evars isevars env l = List.fold_left |