aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/ascent.mli
Commit message (Collapse)AuthorAge
* modif des fixpoints pour que si on donne une notation au produit, les pts ↵Gravatar barras2004-03-05
| | | | | | fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
* takes better account of the new possibility to pass a parametric count argumentGravatar bertot2004-03-03
| | | | | | | to both 'do' and 'fail' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5425 85f007b7-540e-0410-9357-904b9bb8a0f7
* makes sure the following examples are well-treated:Gravatar bertot2004-02-19
| | | | | | | | | | | | | | | | | | | | | | Export X. conditional trivial rewrite nat_le_correct in H. firstorder. Definition error := @None. Proof with trivial. Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l with minus := Rminus div := Rdiv. Ltac ElimPcompare c1 c2 := let x := fresh H in intro x. simplify_eq H. Extraction Inline list_length_induction. Extraction NoInline code insert isort map frequency_list huffman encode decode. ajoute une modification dans le traitement de let_tuple git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5363 85f007b7-540e-0410-9357-904b9bb8a0f7
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
| | | | | | | | | - fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
* accomodate the .. extensionGravatar bertot2004-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5350 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds the possibility to have terms (and not just identifiers) as hintsGravatar bertot2004-02-13
| | | | | | | Adds the 'Reserved Notation' command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5335 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicits can have an optional list of argument, which is differentGravatar bertot2004-02-12
| | | | | | | | | from an empty list of arguments. in H at 2 |- * was badly translated in clauses (for replacement tactics) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5318 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds the possibility to mark function arguments as formulas in LtacGravatar bertot2004-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5276 85f007b7-540e-0410-9357-904b9bb8a0f7
* updates the definition of tactics using Ltac and adds the subst tacticGravatar bertot2004-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5274 85f007b7-540e-0410-9357-904b9bb8a0f7
* updates the tactics contradiction and autorewrite, the commandsGravatar bertot2004-01-29
| | | | | | | set implicit arguments, hint rewrite, and proof git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5263 85f007b7-540e-0410-9357-904b9bb8a0f7
* make sure that 'in' clauses for reduction tactics are translatedGravatar bertot2004-01-28
| | | | | | | | | | | | | | once again re-organize the way intro patterns are translated: there is now only one kind of pattern that can be used for both and and or constructs: the use of the multiplet notation should only be a matter of notation. un-capitalize a few tactic names for tactics represented using the TacExtend construct. corrects a bug in the way binders or coercion binders were used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5260 85f007b7-540e-0410-9357-904b9bb8a0f7
* a try to make intro patterns betterGravatar bertot2004-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5247 85f007b7-540e-0410-9357-904b9bb8a0f7
* streamlines the keywords for definitions, require commandsbinders, notationGravatar bertot2004-01-24
| | | | | | | | | definitions, Show commands, Print commands, proof starting commands, Search commands, scope commands, type reservation command, locate commands, time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5244 85f007b7-540e-0410-9357-904b9bb8a0f7
* change add path commands to get the extra argument and the Hint commandsGravatar bertot2004-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5239 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixes argument lists for tactic definitions, updates inversion tacticsGravatar bertot2004-01-22
| | | | | | | so that they use intro-pattern-lists like induction and destruct git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5236 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds a clause argument to symmetryGravatar bertot2004-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5235 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds the notations in inductive definitions, improves the consistency betweenGravatar bertot2004-01-22
| | | | | | | | induction et destruct, takes the extra argument for fail and idtac into account git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5233 85f007b7-540e-0410-9357-904b9bb8a0f7
* handles explicit function calls, names meta variables in patternsGravatar bertot2004-01-22
| | | | | | | | | | | | | (in V8 the name is not a number), explicitation of arguments with names (but not with rank anymore), the refine tactic now has its own operator the structure information for hypotheses in induction is now handled as in intro, the tactic instantiate has been modified to use clauses, the wildcard rule for Ltac pattern matching on goals has been added and the possibility to refer to types of values and instantiated contexts in values in Ltac have been added. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5232 85f007b7-540e-0410-9357-904b9bb8a0f7
* updates the structure of fix (struct argument added) and ifGravatar bertot2004-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5225 85f007b7-540e-0410-9357-904b9bb8a0f7
* 1.20Gravatar bertot2004-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5217 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds constructs to handle notations in patternsGravatar bertot2004-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5215 85f007b7-540e-0410-9357-904b9bb8a0f7
* translation to structures now okay for pattern matching constructsGravatar bertot2004-01-15
| | | | | | | The locations in simpl, unfold, and the like are also better taken into account git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5209 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugs avec Pose et AssertGravatar barras2004-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorisation et generalisation des clausesGravatar barras2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
| | | | | | | Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle syntaxe de ltacGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
* all tactics should be covered now: remainsGravatar bertot2003-01-26
| | | | | | | TacAlias, but does not seem to be active code for now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3613 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add translations for many tactics but a dozen are still remainingGravatar bertot2003-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3612 85f007b7-540e-0410-9357-904b9bb8a0f7
* removes all references to ctast.ml the Makefile has been updated accordingly.Gravatar bertot2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a few operators in the new version of xlate.ml and make sureGravatar bertot2003-01-21
| | | | | | | that ast_to_ct is not use anymore in translate_constr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3552 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajoute le bon traitement pour Ring, Locate, CommentsGravatar bertot2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3404 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take notations into account: numbers and the CNotation operator.Gravatar bertot2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvellesGravatar bertot2002-12-03
| | | | | | | syntaxes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3362 85f007b7-540e-0410-9357-904b9bb8a0f7
* correcting the treatment of many tactics that use quant_hyp in file xlate.mlGravatar bertot2002-10-06
| | | | | | | and associated file. Also adding a systematic check approach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Previous version did compile but did not make it possible to actually runGravatar bertot2002-10-03
| | | | | | | | | | | | | | | | | | | | | | | | | pcoq. This version does work. Main modification is: - change centaur.ml4 so that * the Pcoq mode is really started by Start Pcoq Mode. * Reset <id> and Reset Initial work as planned for Pcoq (commands are Pcoq Reset <id> and Pcoq ResetInitial). * current_proof_name() does not raise an exception when there is no current proof. - change xlate.ml so that the main tacticals are translated correctly to pcoq data structures. - change in ascent.mli so that * we make sure Fail can now have a numeric argument, * progress is added - vtp.ml is changed in accordance with ascent.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrating the Ltac language and the Blast tool into the interfaceGravatar bertot2001-12-18
| | | | | | | | | | | | | capabilities: The Ltac language is the language that makes it possible to define new tactics without using the ocaml language (already present in coq for a few months). The Blast tool is a tool that checks whether the goals could be solve automatically and proposes the proof trace to the user. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2313 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-11-05
| | | | | | | | | | - reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
* PrsingGravatar herbelin2001-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding files for the production of textual explanations as used in pcoq.Gravatar bertot2001-04-18
| | | | | | | | | | dependence files are updated accordingly. Modifications in other files to cope with a few errors in the translation for the parser (mostly around records, coercions, and the search-pattern command). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1599 85f007b7-540e-0410-9357-904b9bb8a0f7
* Files that handle the dialogue with the graphical user-interface pcoq.Gravatar bertot2001-04-04
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1531 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 12:34:11 +0000