diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/README | 2 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/InitialRing.v | 16 | ||||
| -rw-r--r-- | plugins/ssr/ssrfun.v | 2 |
4 files changed, 11 insertions, 11 deletions
diff --git a/plugins/cc/README b/plugins/cc/README index c616b5daab..7df7b971e8 100644 --- a/plugins/cc/README +++ b/plugins/cc/README @@ -9,7 +9,7 @@ Files : - ccalgo.ml : congruence closure algorithm - ccproof.ml : proof generation code -- cctac.ml4 : the tactic itself +- cctac.mlg : the tactic itself - CCSolve.v : a small Ltac tactic based on congruence Known Bugs : the congruence tactic can fail due to type dependencies. diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index ef012e5092..f47a14cdc7 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,7 +9,7 @@ (************************************************************************) (* This file uses the (non-compressed) union-find structure to generate *) -(* proof-trees that will be transformed into proof-terms in cctac.ml4 *) +(* proof-trees that will be transformed into proof-terms in cctac.mlg *) open CErrors open Constr diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index a98a963207..dc096554c8 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -828,31 +828,31 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk := end in ring_elements set ext rspec pspec sspec dspec rk ltac:(fun arth ext_r morph p_spec s_spec d_spec => - match type of morph with + lazymatch type of morph with | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => let gen_lemma2_0 := constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth C c0 c1 cadd cmul csub copp ceq_b phi morph) in - match p_spec with + lazymatch p_spec with | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec => let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in - match d_spec with + lazymatch d_spec with | @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec => let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in - match s_spec with + lazymatch s_spec with | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec => let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in let lemma1 := constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in fun f => f arth ext_r morph lemma1 lemma2 - | _ => fail 4 "ring: bad sign specification" + | _ => fail "ring: bad sign specification" end - | _ => fail 3 "ring: bad coefficient division specification" + | _ => fail "ring: bad coefficient division specification" end - | _ => fail 2 "ring: bad power specification" + | _ => fail "ring: bad power specification" end - | _ => fail 1 "ring internal error: ring_lemmas, please report" + | _ => fail "ring internal error: ring_lemmas, please report" end). (* Tactic for constant *) diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 0ce3752a51..dc774e811e 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -166,7 +166,7 @@ Require Import ssreflect. right_loop inv op <-> op, inv obey the inverse loop right axiom: (x op y) op (inv y) = x for all x, y. rev_right_loop inv op <-> op, inv obey the inverse loop reverse right - axiom: (x op y) op (inv y) = x for all x, y. + axiom: (x op (inv y)) op y = x for all x, y. Note that familiar "cancellation" identities like x + y - y = x or x - y + y = x are respectively instances of right_loop and rev_right_loop The corresponding lemmas will use the K and NK/VK suffixes, respectively. |