aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.ml
Commit message (Collapse)AuthorAge
* Modification de la vm:Gravatar notin2007-03-27
| | | | | | | | | | | | | | | - le type val_kind n'embarque plus le constr (pb de cohérence avec le context); - en revanche, lors du calcul d'une valeur, on calcule aussi l'ensemble des variables nommées dont la valeur peut dépendre; - lors du clear_hyps, si la valeur dépend d'une variable effacée, on invalide le calcul. Corrige le bug #1419 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9733 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESGravatar herbelin2007-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans check_and_clear_in_constr + simplification deGravatar notin2007-01-31
| | | | | | | | la gestion des erreurs dans clear_hyps. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle implantation de clear_hypsGravatar notin2007-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9560 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1315:Gravatar notin2007-01-22
| | | | | | | | | | | | | | | | | | - ajouts des opérations clear_evar_hyps_in_evar, clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui permettent de supprimer des hypothèses dans le contexte des evars, en créant une nouvelle evar avec un contexte restreint; - adaptation de clear_hyps dans Logic pour qu'elle mette à jour le contexte des evars; - adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié; - déplacement de la tactique Change_evars dans prim_rule. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur suppression des vars anonymes des contextes d'evars (echec ↵Gravatar herbelin2006-12-12
| | | | | | Case15.v et CasesDep.v pas anormal) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
| | | | | | | | | | cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml) + test régression bug #1041 + allègement syntaxe tactique evar + essai de ne pas faire dépendre les evars des variables anonymes afin de résoudre le bug #932 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mort (duplication de code dans reductionops.ml)Gravatar herbelin2006-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9388 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
| | | | | | | | | | | | en dernière étape de la procédure d'unification - Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution de l'unification premier ordre flexible/rigide - Déplacement check_evars dans Evarutil Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ? (cf exemples d'application dans test-suite/success/evars.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout unification pattern dans l'algorithme d'unification desGravatar herbelin2006-09-12
| | | | | | | tactiques (unification.ml) + renommages (evarconv.ml) + exemple (unification.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout (pour complétude) du cas d'inversion d'un pattern de Miller visGravatar herbelin2006-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'Gravatar herbelin2006-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
* Diverses modifications autour de l'unification modulo conversion:Gravatar herbelin2006-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
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for new unification, not used in default version as it really changes ↵Gravatar msozeau2006-04-10
| | | | | | unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun ↵Gravatar msozeau2006-04-10
| | | | | | | | | | | (previous and current version work). Changed the type of typing constraints so as to have all the necessary information on abstract tycons. Updates of subtac to use the new type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
| | | | | | | | | | - Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Orthographe de 'instantiate'Gravatar herbelin2005-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* backtrack sur le typage des instantiations d\'evarsGravatar barras2005-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7129 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparations de quelques petits bugs d\'unification + introduction de la ↵Gravatar barras2005-06-07
| | | | | | notion de variable de sortes (mais pas encore utilise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7120 85f007b7-540e-0410-9357-904b9bb8a0f7
* essai de typage des instantiations d\'evarsGravatar barras2005-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
* eradication de Evarutil.w_DefineGravatar barras2005-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7113 85f007b7-540e-0410-9357-904b9bb8a0f7
* assouplissement de real_clean: ne tient pas compte des occcurences flexibles ↵Gravatar barras2005-06-05
| | | | | | des variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7112 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification: evar_define checks the free variables are bound in the evar contextGravatar barras2005-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7088 85f007b7-540e-0410-9357-904b9bb8a0f7
* WARNING: unification changed (to fix a bug).Gravatar sacerdot2005-05-24
| | | | | | | | | | | | | | | | | 1. When matching ?i[sigma] against t' in some cases ?i was instantiated with t' ignoring the explicit substitution sigma (i.e. always doing mimick); however, when t' occurs in sigma ?i can be instatiated with a Var/Rel (i.e. doing projection). The new behaviour is not equivalent to the old one (even up to bugs) since the new behaviour may accept not well typed instantiations and fail only later whereas the old (but buggy) behaviour failed immediately. 2. Second bug fixed: it was the case that instantiating and evar doing projection did not check whether the body of the evar contained metavariables (that breaks a Coq invariant). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack version 1.82 awaiting for better understanding of the consequences ↵Gravatar herbelin2005-03-12
| | | | | | of removing Anonymous from evars contexts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Méthode plus raisonnable pour supprimer l'inefficacité des evars ↵Gravatar herbelin2005-03-11
| | | | | | dépendantes de Anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6825 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #931 (continued): no recursion on the evars instantiationGravatar herbelin2005-03-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6816 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #931: leave dependent evars as such for refineGravatar herbelin2005-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2005-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement correction bug do_restrict_hys: ne pas inverser les argumentsGravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6454 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug historique de do_restrict_hyps + code mortGravatar herbelin2004-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6435 85f007b7-540e-0410-9357-904b9bb8a0f7
* C'est trop compliqué de mettre à jour les types du metamap en passant sous ↵Gravatar herbelin2004-12-06
| | | | | | les lieurs, plus simple de garder le type avec un cast (cf bug #889) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6415 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
* hiding the meta_map in evar_defsGravatar barras2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification encore...Gravatar barras2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit bug avec les effets de bordsGravatar barras2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6078 85f007b7-540e-0410-9357-904b9bb8a0f7
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #794: conv made in wrong envGravatar barras2004-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5897 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #790: better error_not_cleanGravatar barras2004-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5896 85f007b7-540e-0410-9357-904b9bb8a0f7
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation d'une rupture (en presence de types implicites) de l'invariant ↵Gravatar herbelin2004-01-29
| | | | | | que les variables liees sont toujours nommees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5268 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 21:43:06 +0000