coq/plugins/setoid_ring/vo.itarget, branch master The formal proof system Remove remaining vo.itarget files (obsolete since PR #499) 2017-06-10T14:13:54+00:00 Pierre Letouzey 2017-06-10T14:13:54+00:00 79c42e22dd5106dcb85229ceec75331029ab5486 






Legacy Ring and Legacy Field migrated to contribs
2012-07-05T22:51:11+00:00

letouzey

2012-07-05T22:51:11+00:00

2ed6aeb03fc0e25a47223189d8444cbb6b749f2d

 One slight point to check someday : fourier used to
 launch a tactic called Ring.polynom in some cases.
 It it crucial ? If so, how to replace with the setoid_ring
 equivalent ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7





 One slight point to check someday : fourier used to
 launch a tactic called Ring.polynom in some cases.
 It it crucial ? If so, how to replace with the setoid_ring
 equivalent ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7







moins de reification inutile, noatations standards
2011-08-04T15:22:08+00:00

pottier

2011-08-04T15:22:08+00:00

ca6b6bfde9a0c5b91a53e9c139140403369ff658

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7







Ring2 devient Ncring et la reification par les type classes est partagee
2011-07-26T12:36:53+00:00

pottier

2011-07-26T12:36:53+00:00

077019d1bef2598d4dd1884712a1ee73d39d59fd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14298 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14298 85f007b7-540e-0410-9357-904b9bb8a0f7







ring2, cring, nsatz avec type classe avec parametres plus notations
2011-06-10T09:24:20+00:00

pottier

2011-06-10T09:24:20+00:00

931f3c2f0aa5a4c6936b9b269e146df402d8e383

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14175 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14175 85f007b7-540e-0410-9357-904b9bb8a0f7







Revert "syntax for exponents"
2011-02-25T14:19:39+00:00

glondu

2011-02-25T14:19:39+00:00

f81ff03b1c2d66e39caa741e7543a9e12b5a51a0

This reverts pottier's commit r13849. It references a
ncring_plugin.cma for which there is no rule. I guess he forgot to
commit something...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13856 85f007b7-540e-0410-9357-904b9bb8a0f7





This reverts pottier's commit r13849. It references a
ncring_plugin.cma for which there is no rule. I guess he forgot to
commit something...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13856 85f007b7-540e-0410-9357-904b9bb8a0f7







syntax for exponents
2011-02-22T14:00:38+00:00

pottier

2011-02-22T14:00:38+00:00

4a2bd45d6b3c2adc90ac547f5afc0ebdd51c3293

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7







anneaux commutatifs ou non, reification sans ml
2011-02-22T12:39:35+00:00

pottier

2011-02-22T12:39:35+00:00

81dd7a1db170d7d10d8a378cfd0719c2ded3f7df

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13848 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13848 85f007b7-540e-0410-9357-904b9bb8a0f7







Factorisation between Makefile and ocamlbuild systems : .vo to compile are in */*/vo.itarget
2009-12-09T16:45:42+00:00

letouzey

2009-12-09T16:45:42+00:00

cfc9e109a653047b7ca73224525bba67a8c3a571

 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7





 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7