coq/contrib, branch master

Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

2009-03-20T01:22:58+00:00

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

fixed ring/field warning about hyp cleaning up

2009-03-18T14:47:35+00:00

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

Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)

2009-03-17T21:07:50+00:00

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

- gros commit sur ring et field: passage des arguments simplifie

2009-03-17T20:14:19+00:00

- tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient
  pas evalues, laissant des variables libres (symptome: exc Not_found)
- reals: Open Local --> Local Open
- ListTactics: syntaxe des listes



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

Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"

2009-03-16T08:18:53+00:00

now works correctly, "unfold foo at 4 in H at 3" now fails correctly,
etc.). The terminology for clauses (though I don't find the term
"clause" very intuitive after all) is mostly preserved except for
"simple_clause" which becomes a light form of "clause" instead of
being an atom of clause (what played the role of "simple_clause" is
now called "goal_location" - better names are welcome).
Main changes are in tacticals.ml and tactics.ml.



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

Cleaning/uniformizing the interface of tacticals.mli

2009-03-14T21:29:19+00:00

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

Makefile: ml dependencies of contribs are moved to .mllib files

2009-03-14T11:29:46+00:00

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

Cleanup: remove old correctness files, unused for a long time

2009-03-11T13:36:35+00:00

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

fixed groebner as a plugin + pattern matching Timeout

2009-03-06T21:40:38+00:00

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

missing Require

2009-03-06T14:28:03+00:00

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