aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
* RienGravatar herbelin2000-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifs de presentation.Gravatar delahaye2000-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@520 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage EAuto et RingGravatar filliatr2000-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de GenericGravatar herbelin2000-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@476 85f007b7-540e-0410-9357-904b9bb8a0f7
* DocGravatar herbelin2000-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug (typage avec meta)Gravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@442 85f007b7-540e-0410-9357-904b9bb8a0f7
* docGravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@434 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement nettoyage PfeditGravatar herbelin2000-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@415 85f007b7-540e-0410-9357-904b9bb8a0f7
* compilation bytecode / native :Gravatar filliatr2000-05-03
| | | | | | | | | | - script de configuration - Makefile - simplification de coqmktop - option -opt de coqc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Completion d'un match non exhaustifGravatar delahaye2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@411 85f007b7-540e-0410-9357-904b9bb8a0f7
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage Omega (mais toujours pas Zpower et Zlogarithm)Gravatar filliatr2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'Gravatar herbelin2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@394 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite intégration de constr_patternGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@393 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage bdize -> ast_of_constrGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@385 85f007b7-540e-0410-9357-904b9bb8a0f7
* Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@382 85f007b7-540e-0410-9357-904b9bb8a0f7
* chgt unify_0Gravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@378 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en ↵Gravatar herbelin2000-03-28
| | | | | | {pf_,}interp_constr* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de type_of_case, type_case_branches, etcGravatar herbelin2000-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement plain_instance en instance qui n'a plus besoin de envGravatar herbelin2000-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@340 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'Gravatar herbelin2000-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@322 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentationGravatar filliatr2000-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@288 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction de l'implémentation des signatures de Sign en vue intégration ↵Gravatar herbelin2000-01-26
| | | | | | du let-in git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage command en constrGravatar herbelin2000-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
| | | | | | | | | les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@254 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug mk_clenv_from lorsque pas d argumentsGravatar filliatr1999-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@252 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour de refiner.ml (reports de modifs de la V6.3)Gravatar barras1999-12-13
| | | | | | | bug possible dans lib.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@250 85f007b7-540e-0410-9357-904b9bb8a0f7
* - états fabriqués avec -silentGravatar filliatr1999-12-13
| | | | | | | | | - compilation theories avec -q - correction but de tclORELSE qui doit maintenant rattraper aussi TypeError et RefinerError git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@249 85f007b7-540e-0410-9357-904b9bb8a0f7
* - méthode load sur les HintsGravatar filliatr1999-12-13
| | | | | | | | - CAST pris en compte dans Astterm - Coercin.lookup_path_to_sort_from protégé par un try/with git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@248 85f007b7-540e-0410-9357-904b9bb8a0f7
* - erreurs PretypeGravatar filliatr1999-12-10
| | | | | | | - Write / Restore State git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@230 85f007b7-540e-0410-9357-904b9bb8a0f7
* debug resetGravatar filliatr1999-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@229 85f007b7-540e-0410-9357-904b9bb8a0f7
* - constantes avec recettesGravatar filliatr1999-12-09
| | | | | | | | - discharge en deux temps, avec état remis comme au début de la section (mais c'est toujours buggé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
* premier debugageGravatar filliatr1999-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coqmktopGravatar filliatr1999-12-03
| | | | | | | - #use "include.ml";; git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@198 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules profile, Coqinit et Coqtop (=main)Gravatar filliatr1999-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7
* - global_reference traite des variablesGravatar filliatr1999-12-03
| | | | | | | | | - construct_reference, avec environnement en argument - link de Class - Definition et Check au toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@193 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 18:29:28 +0000