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






Accomodating #4166 (providing "Require Import OmegaTactic" as a
2015-04-01T20:46:17+00:00

Hugo Herbelin

2015-03-30T20:15:02+00:00

8581e1a977518c354eb06820d3513238412af7de

replacement for 8.4's "Require Omega").





replacement for 8.4's "Require Omega").







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