coq/contrib/firstorder, 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

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

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

pushed evar reduction in kernel

2009-02-06T21:25:52+00:00

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

Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->

2008-12-31T10:57:09+00:00

splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
shortcuts for "fst (decompose_prod t)" and co.




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

Fixes and refinements regarding occurrence selection:

2008-10-26T19:22:27+00:00

- make the modifiers "value of" and "type of" for "set" working (it was not!),
- clear unselected hypotheses in the "in" clause of "induction/destruct" when
  the destructed term is a variable (experimental),
- support for generalization of hypotheses in the induction hypotheses using
  the "in" clause of "induction" (e.g. "induction n in m, H" will
  generalize over m -- would it be better to have an explicit 
  "over"/"generalizing" clause ?).
Added clause "as" to "apply in".



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

Enhanced discrimination nets implementation, which can now work with

2008-06-27T15:52:05+00:00

goals containing existentials and use transparency information on
constants (optionally). Only used by the typeclasses eauto engine for
now, but could be used for other hint bases easily (just switch a boolean).
Had to add a new "creation" hint to be able to set said boolean upon
creation of the typeclass_instances hint db.
Improve the proof-search algorithm for Morphism, up to 10 seconds
gained in e.g. Field_theory, Ring_polynom. Added a morphism
declaration for [compose].
One needs to declare more constants as being unfoldable using
the [Typeclasses unfold] command so that discrimination is done correctly, but
that amounts to only 6 declarations in the standard library.


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

- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)

2008-06-10T19:35:23+00:00

- Changement au passage de la convention "at -n1 ... -n2" en 
  "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
  pas mélanger des positifs et des négatifs.
- Au passage:
  - simplification de gclause avec fusion de onconcl et concl_occs,
  - généralisation de l'utilisation de la désignation des occurrences par la
    négative aux cas de setoid_rewrite, clrewrite et rewrite at,
  - correction d'un bug de "rewrite in at" qui utilisait le at de la
    conclusion dans les hyps.


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

- Parameterize unification by two sets of transparent_state, one for open

2008-04-21T13:57:03+00:00

term unification (for constant and variable delta unfolding) and one to
parameterize closed-term conversion. Most of the time conversion uses
full delta and unification does no delta. This fine-grain is used in
rewrite/setoid_rewrite, where only closed-term delta on global constants
is allowed.
- Interpret Hint Unfold as a directive for delta conversion in
auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints).
- Remove ad-hoc support for this in typeclasses. Now setoid_rewrite
works correctly w.r.t. the old version regarding local definitions.
- Fix closed bugs which needed updating due to syntax modifications.


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

first-order --> firstorder (kills a warning about not being a valid id)

2008-04-16T20:40:19+00:00

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