coq/translate, branch master

Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_new en G_.ml + autres petites modifications liées à suppression du traducteur

2005-12-26T20:07:21+00:00

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

Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)

2005-12-26T13:51:24+00:00

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

Simplifification de vernac_expr li l'abandon du traducteur

2005-12-23T10:43:37+00:00

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

Correction pr_module pour traducteur

2005-12-23T10:06:29+00:00

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

Restructuration des points d'entrée de Pretyping et Constrintern

2005-12-21T15:06:11+00:00

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

Changement des named_context

2005-12-02T10:01:15+00:00

Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs


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

Nettoyage suite à la détection par défaut des variables inutilisées par ocaml 3.09

2005-11-08T17:14:52+00:00

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

- debugging og "Show Intros": no line breaking + fresh ids

2005-11-08T11:16:57+00:00

- added the command "Show Match t" which prints a typical
  "match...with" for type t.


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

New command: "Print Ltac qualid" to print user defined tactics.

2005-05-20T16:14:52+00:00

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

Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux niveaux syntaxiques des tacticielles

2005-05-17T12:43:22+00:00

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