diff options
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3943.v | 50 |
2 files changed, 51 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4bde427b1..cb0f66730 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -527,10 +527,10 @@ let top_sort evm undefs = let tosee = ref undefs in let rec visit ev evi = let evs = Evarutil.undefined_evars_of_evar_info evm evi in + tosee := Evar.Map.remove ev !tosee; Evar.Set.iter (fun ev -> if Evar.Map.mem ev !tosee then visit ev (Evar.Map.find ev !tosee)) evs; - tosee := Evar.Map.remove ev !tosee; l' := ev :: !l'; in while not (Evar.Map.is_empty !tosee) do diff --git a/test-suite/bugs/closed/3943.v b/test-suite/bugs/closed/3943.v new file mode 100644 index 000000000..5e5ba816f --- /dev/null +++ b/test-suite/bugs/closed/3943.v @@ -0,0 +1,50 @@ +(* File reduced by coq-bug-finder from original input, then from 9492 lines to 119 lines *) +(* coqc version 8.5beta1 (January 2015) compiled on Jan 18 2015 7:27:36 with OCaml 3.12.1 + coqtop version 8.5beta1 (January 2015) *) + +Set Typeclasses Dependency Order. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (@paths _ x y) : type_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +Set Implicit Arguments. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. + +Record PreCategory := Build_PreCategory' { + object :> Type; + morphism : object -> object -> Type; + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' }. +Arguments identity {!C%category} / x%object : rename. +Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename. + +Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { + morphism_inverse : morphism C d s; + left_inverse : compose morphism_inverse m = identity _; + right_inverse : compose m morphism_inverse = identity _ }. +Arguments morphism_inverse {C s d} m {_}. +Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope. + +Class Isomorphic {C : PreCategory} s d := { + morphism_isomorphic :> morphism C s d; + isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }. +Coercion morphism_isomorphic : Isomorphic >-> morphism. + +Variable C : PreCategory. +Variables s d : C. + +Definition path_isomorphic (i j : Isomorphic s d) +: @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j. +Admitted. + +Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q +: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
\ No newline at end of file |