aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--contrib/subtac/subtac.ml16
-rw-r--r--ide/coq.ml1
-rw-r--r--test-suite/success/dependentind.v6
-rw-r--r--tools/coqdoc/index.mll10
-rw-r--r--tools/coqdoc/output.ml4
-rw-r--r--toplevel/vernacentries.ml2
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;