aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-09-01Suite ajout option -ocamlib à configurenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9115 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Suite commit 9110 (uniformisation position notation dans les blocs inductifs)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9114 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Suite commit 9110 (uniformisation position notation dans les blocs inductifs)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9113 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Force évaluation 'naturelle' de list_map2_i et list_map3 de gauche à droiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9112 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9111 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Ajout possibilité clause "where" dans co-points fixes herbelin
(+ 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
2006-09-01Affichage de l'aide dans configurenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9109 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Extension et réorganisation de l'interprétation des (co-)points fixesherbelin
- 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
2006-09-01Export de fonctions d'interprétation acceptant des evars non résoluesherbelin
en entrée et en sortie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9107 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Ajout is_sort: test si se réduit en une sorteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9106 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Export de check_evars vers command.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9105 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Indentation + typonotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Ajout iter_rel_context/iter_named_contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9103 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Appel à caml_modify pour Ocaml 3.07notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9102 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Modification du manuel de référence: le flag evar pour cbv n'existe plus.notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9101 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-31Un peu de delta-réduction...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9100 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-30Modification du configure pour paramétrer les exécutables liés à la ↵notin
compilation C git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9099 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-29Compilation de Coq sous Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9098 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-29Ajout (pour complétude) du cas d'inversion d'un pattern de Miller visherbelin
à vis d'une Var nommée. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9097 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-29Prise en compte de l'instance des evars dans la détection des 'motifs'herbelin
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
2006-08-29Changement de l'appel aux exécutables Caml (noms absolus)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9095 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-29Il faut (au moins) normaliser les evars avant de tenterherbelin
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
2006-08-28Passage à une définition de inhabited plus dans les 'standard ↵herbelin
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
2006-08-28improve the amount of information given by the Ltac tactic debuggerbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28"Essai de remplacement de "ex P" par "exists x, P x" suite àherbelin
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
2006-08-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9090 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28Ajout thèse Cornesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9089 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28Diverses modifications autour de l'unification modulo conversion:herbelin
- 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
2006-08-28Ajout whd_eta + export append_stack_list + petit nettoyage (dont maj de herbelin
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
2006-08-28Export de closedn pour Evarutilherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9086 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28Petite optimisation récursive-terminale en passantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9085 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-25two minor bug corrections in General Recursive Functions jforest
and one un structural Functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9084 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-25correction bug vm_computebgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9083 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24Morceau de code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9082 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24Amelioration des messages d'erreur de Fucntion jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9081 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9080 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ JMeq sur Type + typos (sur propositions de Pierre Castéran)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9079 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9078 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24JMeq maintenant applicable sur Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9077 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-23Bug in replace tactics introduced in r9073 (overlap between replace .. with ↵jforest
and replace_term). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9076 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22making otags working jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9075 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22Forgot a file in previous commit jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9074 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22remove an orphan comment (attached to a piece of code that was removed).bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9072 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-17Checks that abstract setoid rings can be defined in a module and the tacticbertot
can be used outside the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9071 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-17corrects an error in the substitution of module paths inside tactics:bertot
objects of the form TacDynamic should not be left unchanged if their content is tagged with "constr". This correction makes that setoid ring can now work with rings that were declared inside a module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9070 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-16+ timide essai pour le traitement des as dans les patterns lors de la ↵jforest
generation des graphes de Function + Correction d'un petit bug dans les lemmes d'inversions de Function + Nettoyage d'hypotheses inutile dans les obligations de preuve de Function (wf et measure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9069 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-16MAJ Rectutorial (P. Castéran)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9068 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-15working on functional induction automation (tactic finduction andcourtieu
fauto, not documented yet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9067 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-14comparison functions should be Defined not Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9066 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:34:44 +0000