diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /plugins/ring | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'plugins/ring')
-rw-r--r-- | plugins/ring/LegacyArithRing.v | 6 | ||||
-rw-r--r-- | plugins/ring/LegacyNArithRing.v | 6 | ||||
-rw-r--r-- | plugins/ring/LegacyRing.v | 4 | ||||
-rw-r--r-- | plugins/ring/LegacyRing_theory.v | 4 | ||||
-rw-r--r-- | plugins/ring/LegacyZArithRing.v | 6 | ||||
-rw-r--r-- | plugins/ring/Ring_abstract.v | 6 | ||||
-rw-r--r-- | plugins/ring/Ring_normalize.v | 15 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring.v | 4 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring_normalize.v | 15 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 4 | ||||
-rw-r--r-- | plugins/ring/g_ring.ml4 | 4 | ||||
-rw-r--r-- | plugins/ring/ring.ml | 57 |
12 files changed, 54 insertions, 77 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index 2de16bc1..fd5bcd93 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (* Instantiation of the Ring tactic for the naturals of Arith $*) Require Import Bool. @@ -17,7 +15,7 @@ Require Import Eqdep_dec. Open Local Scope nat_scope. -Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := +Fixpoint nateq (n m:nat) {struct m} : bool := match n, m with | O, O => true | S n', S m' => nateq n' m' diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v index ae7e62e0..5dcd6d84 100644 --- a/plugins/ring/LegacyNArithRing.v +++ b/plugins/ring/LegacyNArithRing.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyNArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (* Instantiation of the Ring tactic for the binary natural numbers *) Require Import Bool. @@ -16,7 +14,7 @@ Require Export ZArith_base. Require Import NArith. Require Import Eqdep_dec. -Unboxed Definition Neq (n m:N) := +Definition Neq (n m:N) := match (n ?= m)%N with | Datatypes.Eq => true | _ => false diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v index e53e60d3..d19e9f58 100644 --- a/plugins/ring/LegacyRing.v +++ b/plugins/ring/LegacyRing.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyRing.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Export Bool. Require Export LegacyRing_theory. Require Export Quote. diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v index bf61aee1..ca3355a6 100644 --- a/plugins/ring/LegacyRing_theory.v +++ b/plugins/ring/LegacyRing_theory.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyRing_theory.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Export Bool. Set Implicit Arguments. diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v index d1412104..5845062d 100644 --- a/plugins/ring/LegacyZArithRing.v +++ b/plugins/ring/LegacyZArithRing.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyZArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (* Instantiation of the Ring tactic for the binary integers of ZArith *) Require Export LegacyArithRing. @@ -15,7 +13,7 @@ Require Export ZArith_base. Require Import Eqdep_dec. Require Import LegacyRing. -Unboxed Definition Zeq (x y:Z) := +Definition Zeq (x y:Z) := match (x ?= y)%Z with | Datatypes.Eq => true | _ => false diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v index e6e2dda9..1763d70a 100644 --- a/plugins/ring/Ring_abstract.v +++ b/plugins/ring/Ring_abstract.v @@ -1,19 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring_abstract.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import LegacyRing_theory. Require Import Quote. Require Import Ring_normalize. -Unset Boxed Definitions. - Section abstract_semi_rings. Inductive aspolynomial : Type := diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index dd4e7314..c6dff3e0 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -1,18 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring_normalize.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import LegacyRing_theory. Require Import Quote. Set Implicit Arguments. -Unset Boxed Definitions. Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. Proof. @@ -749,11 +746,11 @@ Qed. (* End properties. *) End semi_rings. -Implicit Arguments Cons_varlist. -Implicit Arguments Cons_monom. -Implicit Arguments SPconst. -Implicit Arguments SPplus. -Implicit Arguments SPmult. +Arguments Cons_varlist : default implicits. +Arguments Cons_monom : default implicits. +Arguments SPconst : default implicits. +Arguments SPplus : default implicits. +Arguments SPmult : default implicits. Section rings. diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v index da4e3756..106a946d 100644 --- a/plugins/ring/Setoid_ring.v +++ b/plugins/ring/Setoid_ring.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Setoid_ring.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Export Setoid_ring_theory. Require Export Quote. Require Export Setoid_ring_normalize. diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index c4527cfb..ad75a8a4 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -1,18 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Setoid_ring_normalize.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import Setoid_ring_theory. Require Import Quote. Set Implicit Arguments. -Unset Boxed Definitions. Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. Proof. @@ -1014,11 +1011,11 @@ Qed. End semi_setoid_rings. -Implicit Arguments Cons_varlist. -Implicit Arguments Cons_monom. -Implicit Arguments SetSPconst. -Implicit Arguments SetSPplus. -Implicit Arguments SetSPmult. +Arguments Cons_varlist : default implicits. +Arguments Cons_monom : default implicits. +Arguments SetSPconst : default implicits. +Arguments SetSPplus : default implicits. +Arguments SetSPmult : default implicits. diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index f07cbaf6..dd722f80 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Setoid_ring_theory.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Export Bool. Require Export Setoid. diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 index c5a33f39..e306a531 100644 --- a/plugins/ring/g_ring.ml4 +++ b/plugins/ring/g_ring.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: g_ring.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Quote open Ring open Tacticals diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 6e67272c..98d6361c 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ring.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* ML part of the Ring tactic *) open Pp @@ -21,7 +19,6 @@ open Reductionops open Tacticals open Tacexpr open Tacmach -open Proof_trees open Printer open Equality open Vernacinterp @@ -138,7 +135,7 @@ let mkLApp(fc,v) = mkApp(Lazy.force fc, v) module OperSet = Set.Make (struct type t = global_reference - let compare = (Pervasives.compare : t->t->int) + let compare = (RefOrdered.compare : t->t->int) end) type morph = @@ -169,7 +166,7 @@ type theory = (* Theories are stored in a table which is synchronised with the Reset mechanism. *) -module Cmap = Map.Make(struct type t = constr let compare = compare end) +module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) let theories_map = ref Cmap.empty @@ -265,7 +262,7 @@ let subst_th (subst,(c,th as obj)) = (c',th') -let (theory_to_obj, obj_to_theory) = +let theory_to_obj : constr * theory -> obj = let cache_th (_,(c, th)) = theories_map_add (c,th) in declare_object {(default_object "tactic-ring-theory") with open_function = (fun i o -> if i=1 then cache_th o); @@ -380,8 +377,14 @@ Builds *) +module Constrhash = Hashtbl.Make + (struct type t = constr + let equal = eq_constr + let hash = hash_constr + end) + let build_spolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) (* aux creates the spolynom p by a recursive destructuration of c @@ -395,14 +398,14 @@ let build_spolynom gl th lc = | _ when closed_under th.th_closed c -> mkLApp(coq_SPconst, [|th.th_a; c |]) | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -437,7 +440,7 @@ Builds *) let build_polynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = @@ -458,14 +461,14 @@ let build_polynom gl th lc = | _ when closed_under th.th_closed c -> mkLApp(coq_Pconst, [|th.th_a; c |]) | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -501,7 +504,7 @@ Builds *) let build_aspolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) (* aux creates the aspolynom p by a recursive destructuration of c @@ -515,13 +518,13 @@ let build_aspolynom gl th lc = | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0 | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1 | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -555,7 +558,7 @@ Builds *) let build_apolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = @@ -575,14 +578,14 @@ let build_apolynom gl th lc = | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0 | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_AP1 | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_APvar, [| path_of_int !counter |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -616,7 +619,7 @@ Builds *) let build_setpolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = @@ -637,14 +640,14 @@ let build_setpolynom gl th lc = | _ when closed_under th.th_closed c -> mkLApp(coq_SetPconst, [| th.th_a; c |]) | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -683,7 +686,7 @@ Builds *) let build_setspolynom gl th lc = - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) let rec aux c = @@ -695,14 +698,14 @@ let build_setspolynom gl th lc = | _ when closed_under th.th_closed c -> mkLApp(coq_SetSPconst, [| th.th_a; c |]) | _ -> - try Hashtbl.find varhash c + try Constrhash.find varhash c with Not_found -> let newvar = mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in begin incr counter; varlist := c :: !varlist; - Hashtbl.add varhash c newvar; + Constrhash.add varhash c newvar; newvar end in @@ -823,9 +826,9 @@ let raw_polynom th op lc gl = (tclTHENS (tclORELSE (Equality.general_rewrite true - Termops.all_occurrences false c'i_eq_c''i) + Termops.all_occurrences true false c'i_eq_c''i) (Equality.general_rewrite false - Termops.all_occurrences false c'i_eq_c''i)) + Termops.all_occurrences true false c'i_eq_c''i)) [tac])) else (tclORELSE |