coq/plugins/micromega/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 






extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/MExtraction.v"
2017-06-01T08:24:10+00:00

Matej Kosik

2017-03-23T13:42:24+00:00

466e6a97c97e83679d49f0867d8f571402e1548f












micromega : more robust generation of proof terms
2016-09-07T08:28:07+00:00

Frédéric Besson

2016-09-07T08:28:07+00:00

6e847be2a6846ab11996d2774b6bc507a342a626

- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
  (This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)





- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
  (This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)







plugin micromega : nra also handles non-linear rational arithmetic over Q (Fixed #4985)
2016-08-30T15:59:59+00:00

Frédéric Besson

2016-08-30T15:12:27+00:00

721637c98514a77d05d080f53f226cab3a8da1e7

Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.





Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.







micromega: removal of spurious Export; addition of Lia.v encapsulating lia and nia.
2013-12-20T00:22:45+00:00

Frédéric Besson

2013-12-20T00:22:45+00:00

ca1305a0187653edcf63e46b84c65130ac78d117












micromega: remove empty file CheckerMaker
2013-08-22T14:29:39+00:00

letouzey

2013-08-22T14:29:39+00:00

676f8fac28958d141a73dd56d087ecdbe046ab31

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





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16724 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