diff options
| -rw-r--r-- | contrib/subtac/subtac.ml | 16 | ||||
| -rw-r--r-- | ide/coq.ml | 1 | ||||
| -rw-r--r-- | test-suite/success/dependentind.v | 6 | ||||
| -rw-r--r-- | tools/coqdoc/index.mll | 10 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
6 files changed, 20 insertions, 19 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index acf1ae838..d10c8f68c 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -104,13 +104,9 @@ let declare_assumption env isevars idl is_coe k bl c nl = errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") -let dump_definition (loc, id) s = - Dumpglob.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) - (string_of_id id)) - let dump_constraint ty ((loc, n), _, _) = match n with - | Name id -> dump_definition (loc, id) ty + | Name id -> Dumpglob.dump_definition (loc, id) false ty | Anonymous -> () let dump_variable lid = () @@ -120,7 +116,7 @@ let vernac_assumption env isevars kind l nl = List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun lid -> - if global then dump_definition lid "ax" + if global then Dumpglob.dump_definition lid (not global) "ax" else dump_variable lid) idl; declare_assumption env isevars idl is_coe kind [] c nl) l @@ -138,7 +134,7 @@ let subtac (loc, command) = match command with | VernacDefinition (defkind, (_, id as lid), expr, hook) -> check_fresh lid; - dump_definition lid "def"; + Dumpglob.dump_definition lid false "def"; (match expr with | ProveBody (bl, t) -> if Lib.is_modtype () then @@ -151,12 +147,12 @@ let subtac (loc, command) = | VernacFixpoint (l, b) -> List.iter (fun ((lid, _, _, _, _), _) -> check_fresh lid; - dump_definition lid "fix") l; + Dumpglob.dump_definition lid false "fix") l; let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l b) | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) -> - dump_definition id "prf"; + Dumpglob.dump_definition id false "prf"; if not(Pfedit.refining ()) then if lettop then errorlabstrm "Subtac_command.StartProof" @@ -176,7 +172,7 @@ let subtac (loc, command) = | VernacCoFixpoint (l, b) -> if Dumpglob.dump () then - List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l; + List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; ignore(Subtac_command.build_corecursive l b) (*| VernacEndProof e -> diff --git a/ide/coq.ml b/ide/coq.ml index c4b6c34b2..2c8d7b8db 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -273,6 +273,7 @@ let rec attribute_of_vernac_command = function (* Commands *) | VernacDeclareTacticDefinition _ -> [] + | VernacCreateHintDb _ -> [] | VernacHints _ -> [] | VernacSyntacticDefinition _ -> [] | VernacDeclareImplicits _ -> [] diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 3f315ccb7..d12c21b15 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -58,11 +58,13 @@ Inductive term : ctx -> type -> Type := Hint Constructors term : lambda. +Open Local Scope context_scope. + Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope. Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> forall τ', term (Γ ,, τ' ;; Δ) τ. -Proof with simpl in * ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda. +Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda. intros Γ Δ τ H. dependent induction H. @@ -81,7 +83,7 @@ Proof with simpl in * ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda Qed. Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ. -Proof with simpl in * ; simplify_dep_elim ; simplify_IH_hyps ; auto. +Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto. intros until 1. dependent induction H. diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 5b5425590..b41c19ac3 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -66,18 +66,20 @@ let full_ident sp id = let add_def loc ty sp id = Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)); - Hashtbl.add deftable (!current_library, id) (Def (full_ident sp id, ty)) + Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty)) let add_ref m loc m' sp id ty = - Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)) + if Hashtbl.mem reftable (m, loc) then () + else + Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)) let add_mod m loc m' id = Hashtbl.add reftable (m, loc) (Mod (m', id)); - Hashtbl.add deftable (m, id) (Mod (m', id)) + Hashtbl.add deftable id (Mod (m', id)) let find m l = Hashtbl.find reftable (m, l) -let find_string m s = Hashtbl.find deftable (m, s) +let find_string m s = Hashtbl.find deftable s (*s Manipulating path prefixes *) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index a7ed7444a..2d547af79 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -273,8 +273,8 @@ module Latex = struct end else begin if !Cdglobals.interpolate then try reference s (Index.find_string !current_module s) - with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" - else printf "\\coqdocvar{"; raw_ident s; printf "}" + with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" + else (printf "\\coqdocvar{"; raw_ident s; printf "}") end end end diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d4c396d49..8c0e7e05a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -375,7 +375,7 @@ let vernac_assumption kind l nl= let vernac_inductive f indl = if Dumpglob.dump () then List.iter (fun ((lid, _, _, cstrs), _) -> - Dumpglob.dump_definition lid false"ind"; + Dumpglob.dump_definition lid false "ind"; List.iter (fun (_, (lid, _)) -> Dumpglob.dump_definition lid false "constr") cstrs) indl; |