coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Ajout eassumption index	herbelin	2006-09-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9129 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour à un warning en cas de (co-)fixpoint pas totalement mutuel	herbelin	2006-09-09
\| \| \| \| \| \| \| \| \|	(après tout, d'autres exemples de non totalement mutuels sont acceptés sans problème par la test de bonne fondation - cf add1/add2 dans Sophia-Antipolis/MATHS/GROUPS/Z et Sophia-Antipolis/HARDWARE) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9128 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating the doc about Function and co	courtieu	2006-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9127 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement, interdiction des points fixes non totalement mutuellement	herbelin	2006-09-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	récursifs parce ce que la condition de garde élimine les appels récursifs sur des sous-termes qui, par construction des types inductifs, ne peuvent ultimement retomber sur un objet du type initial de l'argument de décroissance (p.ex. un appel récursif sur p:positive provenant d'un filtrage sur un z:Z ne sera d'emblée pas considérer sous-terme car la destruction d'un positive ne donnera jamais un Z -- cf exemple de addZ dans une version d'avant aujourd'hui de Sophia-Antipolis/MATHS/GROUPS/Z/Zadd.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9126 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Code mort	herbelin	2006-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9125 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Workaround Map.fold semantic change in ocaml-3.08.4 and higher.	msozeau	2006-09-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9122 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix wrong order for building library, add informative messages.	msozeau	2006-09-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9121 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New handling of obligations.	msozeau	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9120 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug d'ordonnancement des hyps d'induction dans induction/destruct	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9119 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forgot to add this one.	msozeau	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9118 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Subtac fixes, new way of handling obligations in progress.	msozeau	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9117 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq ne compile plus avec OCaml 3.06 (mais avec 3.07 c'est ok)	notin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9116 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite ajout option -ocamlib à configure	notin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9115 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9114 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Force évaluation 'naturelle' de list_map2_i et list_map3 de gauche à droite	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9111 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout possibilité clause "where" dans co-points fixes	herbelin	2006-09-01
\| \| \| \| \| \| \|	(+ uniformisation position notation dans les blocs inductifs et récursifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage de l'aide dans configure	notin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension et réorganisation de l'interprétation des (co-)points fixes	herbelin	2006-09-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Relâchement de l'exigence que les types des paramètres et le type des (co-)points fixes soient donnés. Ils peuvent maintenant être inférés à partir des autres informations de types. - Plus de déclaration séparée de celles des fonctions d'un bloc de points fixes qui n'interviennent pas dans la définition des autres (collect_non_rec): remplacement par un simple warning en cas de non dépendance mutuelle de toutes les fonctions du bloc (de toutes façons les fonctions qui intervenaient dans les autres sans en dépendre - càd les fonctions définissables avant la partie point fixe - n'étaient pas détectées) - Ajout du test de dépendance mutuel au cas des co-points fixes Extension et réorganisation de l'interprétation des blocs de définitions (co-)inductives: relâchement de l'exigence que les types des paramètres soient donnés. Ils peuvent maintenant être inférés à partir des autres informations des blocs d'inductifs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9108 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export de fonctions d'interprétation acceptant des evars non résolues	herbelin	2006-09-01
\| \| \| \| \| \| \|	en entrée et en sortie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9107 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout is_sort: test si se réduit en une sorte	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export de check_evars vers command.ml	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9105 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Indentation + typo	notin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout iter_rel_context/iter_named_context	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9103 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Appel à caml_modify pour Ocaml 3.07	notin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9102 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification du manuel de référence: le flag evar pour cbv n'existe plus.	notin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9101 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un peu de delta-réduction...	herbelin	2006-08-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9100 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification du configure pour paramétrer les exécutables liés à la ↵	notin	2006-08-30
\| \| \| \| \| \|	compilation C git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compilation de Coq sous Windows	notin	2006-08-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9098 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout (pour complétude) du cas d'inversion d'un pattern de Miller vis	herbelin	2006-08-29
\| \| \| \| \| \| \| \|	à vis d'une Var nommée. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9097 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte de l'instance des evars dans la détection des 'motifs'	herbelin	2006-08-29
\| \| \| \| \| \| \| \| \| \| \| \| \|	d'unification à la Miller. Ceci devrait garantir la généralité de la solution modulo le problème résiduel de éta : en l'absence d'éta dans le CCI, le choix entre deux instances éta-convertibles distinctes d'une evar, conduira à des solutions non convertibles pour le CCI. Par exemple, le problème suivant, pour c et Q rigides, a deux solutions distinctes non convertibles. "fun (H: forall P:A->Prop, ~ c (fun x => P x)) (K: c (fun x => Q x)) => H _ K" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9096 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de l'appel aux exécutables Caml (noms absolus)	notin	2006-08-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9095 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Il faut (au moins) normaliser les evars avant de tenter	herbelin	2006-08-29
\| \| \| \| \| \| \| \| \|	l'éta-reduction d'une unification pattern (sinon création d'inférences incompatibles, ce qui, dans le cas de Rocq/ALGEBRA, induisa la disparition d'une projection canonique). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9094 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à une définition de inhabited plus dans les 'standard ↵	herbelin	2006-08-28
\| \| \| \| \| \|	mathématiques'; ajout preuve que tous les 'epsilon i P' sont égaux si P habité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9093 85f007b7-540e-0410-9357-904b9bb8a0f7
*	improve the amount of information given by the Ltac tactic debugger	bertot	2006-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
*	"Essai de remplacement de "ex P" par "exists x, P x" suite à	herbelin	2006-08-28
\| \| \| \| \| \| \| \|	l'introduction d'unification de motifs à la Miller permettant une forme restreinte canonique d'unification du second ordre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9090 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout thèse Cornes	herbelin	2006-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9089 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Diverses modifications autour de l'unification modulo conversion:	herbelin	2006-08-28
\| \| \| \| \| \| \| \| \| \| \| \| \|	- extension de l'unification au cas de motifs (au sens de Dale Miller) [appel de solve_pattern_eqn dans evar_conv_x], - correction de bugs présumés dans real_clean et do_restrict_hyp (prise en compte de la taille courante du contexte de de Bruijn), - ajout d'une heuristique de beta-reduction de tete dans real_clean (cf test-suite/success/unification.v), - suppression de certains "try ... with _ => ...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9088 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout whd_eta + export append_stack_list + petit nettoyage (dont maj de	herbelin	2006-08-28
\| \| \| \| \| \| \| \|	certains commentaires historiques, traçables jusqu'à la version 4.1, mais devenus hors à propos suite aux nombreuses modifications du code). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9087 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export de closedn pour Evarutil	herbelin	2006-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9086 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petite optimisation récursive-terminale en passant	herbelin	2006-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	two minor bug corrections in General Recursive Functions	jforest	2006-08-25
\| \| \| \| \| \| \|	and one un structural Functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9084 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction bug vm_compute	bgregoir	2006-08-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9083 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Morceau de code mort	herbelin	2006-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9082 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amelioration des messages d'erreur de Fucntion	jforest	2006-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9081 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ biblio	herbelin	2006-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9080 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ JMeq sur Type + typos (sur propositions de Pierre Castéran)	herbelin	2006-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ biblio	herbelin	2006-08-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9078 85f007b7-540e-0410-9357-904b9bb8a0f7