aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Code mortGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added map_named_contextGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6737 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Indmap and ConstrMap from Libnames to Names for use in CookingGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6736 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout constant printerGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6735 85f007b7-540e-0410-9357-904b9bb8a0f7
* q_*.cmo useless for making coqtopGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added bigint printerGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6733 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6731 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test bug #922Gravatar herbelin2005-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #922 (problème dans depend) + formattage débogueurGravatar herbelin2005-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage entiers négatifsGravatar herbelin2005-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6726 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6724 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6722 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6720 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6718 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6716 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle mouture Print Canonical StructuresGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6714 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation de destApplication en destAppGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation de destApplication en destApp; simplification decompose_appGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6709 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du reset des numéros d'états dans reset_initial. Plus propreGravatar coq2005-02-10
| | | | | | | pour proofgeneral. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6706 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6704 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6702 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6700 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des ↵Gravatar coq2005-02-07
| | | | | | jours de calcul (chapitre 16, thm prime_2333); peut-être à cause de Z_of_nat??) [HH] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage rawconstrGravatar herbelin2005-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6696 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6694 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6690 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation des libraries compilées uniquement via la structure du ↵Gravatar herbelin2005-02-05
| | | | | | loadpath (sinon des modules de même nom chargés via un Export sont trouvés avant ceux officiellement dans le chemin) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6689 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6687 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug synchronisation fonction connectGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout g_xml.ml4 et cic2Xml.mlGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6684 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout g_xml.ml4 et cic2Xml.mlGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout printer direct cic vers xmlGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export du printer xml vers tacinterpGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout constructeur External pour appel outil externe à CoqGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parseur pour la DTD XML de constr et un peu plus pour les arguments de tactiquesGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout constructeur External pour appel outil externe à CoqGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un processus de communication entre Coq et un outil externeGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'Unboxed des opérations sur positive (cf bug 898)Gravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai d'utilisation de 'where' pour les notationsGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6675 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification des niveaux pr_constr et pr_lconstr en v8 dans pr_prim_rule ↵Gravatar herbelin2005-02-03
| | | | | | (cut, refine, etc était en lconstr par erreur) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6672 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tactics.v bidon pour accomoder make world7Gravatar herbelin2005-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6671 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 01:11:07 +0000