aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppconstr.ml
AgeCommit message (Expand)Author
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-05-29No more Univ in grammar.cmaletouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29Stuff about notation_constr (ex-aconstr) now in notation_ops.mlletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
2012-03-02Noise for nothingpboutill
2012-02-29In the syntax of pattern matching, "in" clauses are patterns.pboutill
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2012-01-19Pretty printing of generalized binderpboutill
2012-01-17Some fix in beautify pretty-printerpboutill
2012-01-10Fix printing of instances, generalized arguments.msozeau
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-07-26Partial revert of r14292pboutill
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
2011-04-24Fixing bug in printing let-in binders in fix/cofixherbelin
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-29Rather quick hack to make basic unicode notations available byherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Removed obsolete v7->v8 translation code (function check_same_type isherbelin
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-05-28Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionaspiwack
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
2008-10-23Open notation for declaring record instances.msozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-10-22A much better implementation of implicit generalization:msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:51:28 +0000