aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-11Another micro-improvement in printing "fix".Hugo Herbelin
Set Printing Width 20. Check fix my_long_fix (my_induction_variable y z t u v w x' y' z' t' u' v' w' : nat) (a b c d e f a' b' c' d' e' f' : bool) := match my_induction_variable with | 0 => 0 | S my_recursive_variable => my_recursive_variable end. gives: fix my_long_fix (my_induction_variable y z t u v w x' y' z' t' u' v' w' : nat) (a b c d e f a' b' c' d' e' f' : bool) {struct my_induction_variable} : nat := match my_induction_variable with | 0 => 0 | S my_recursive_variable => my_recursive_variable end instead of: fix my_long_fix (my_induction_variable y z t u v w x' y' z' t' u' v' w' : nat) (a b c d e f a' b' c' d' e' f' : bool) {struct my_induction_variable} : nat := match my_induction_variable with | 0 => 0 | S my_recursive_variable => my_recursive_variable end
2020-02-11Small improvement to "fix"/"cofix" printing rule.Hugo Herbelin
Set Implicit Arguments. Set Contextual Implicit. Inductive option A := None | Some (a:A). Coercion some_nat := @Some nat. Check fix f x := match x with 0 => None | n => some_nat n end. gives: fix f (x : nat) : option nat := match x with | 0 => None (A:=nat) | S _ => some_nat x end See discussion at https://github.com/coq/coq/pull/11142/files/718c1422954794e0e33a87cf4c9111c00cc186dd#r377054717
2020-02-11Merge PR #11554: Fix #11553: magicaly_constant_of_fixbody checks existence ↵Pierre-Marie Pédrot
of made up constant Reviewed-by: ppedrot
2020-02-11Merge PR #11538: Remove many unsafe_type_of usesPierre-Marie Pédrot
Reviewed-by: Matafou Reviewed-by: gares Reviewed-by: ppedrot
2020-02-09Merge PR #11518: Fix #11515: Ltac2 rewrite on wildcard.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-09Merge PR #11551: Remove -compat 8.9.Emilio Jesus Gallego Arias
Reviewed-by: JasonGross Reviewed-by: ejgallego
2020-02-09Merge PR #11550: Fixing wrong comments in context.mlPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-09Fix #11553: magicaly_constant_of_fixbody checks existence of made up constantGaëtan Gilbert
2020-02-08Remove -compat 8.9.Théo Zimmermann
Commit auto-generated by running dev/tools/update-compat.py --release. As per release doc this must be run at some point before branching (not necessarily close to the branching date).
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
Reviewed-by: herbelin Ack-by: jfehrle
2020-02-08Merge PR #10343: Resolve 10342 : [Ltac2] Add array libraryPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: ppedrot
2020-02-08Merge PR #11404: replace RList by list R in all files where it is used in ↵Pierre-Marie Pédrot
this directory Ack-by: SkySkimmer Reviewed-by: herbelin
2020-02-08Fixing wrong comments in context.ml.Hugo Herbelin
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-02-07Merge PR #11523: [coqdep] Several refactoring and consolidationsGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2020-02-07Remove unsafe_type_of from funindGaëtan Gilbert
2020-02-07various unsafe_type_of -> type_of_variable in funindGaëtan Gilbert
This is the easy part of removing unsafe_type_of, as type_of_variable doesn't return (or even take as argument) an evar map.
2020-02-07Remove confusing commented code in funindGaëtan Gilbert
2020-02-07Merge PR #11528: Checker does not rely on Monomorphic fieldsGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-07[coqdep] Add changelog for recent modifications.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Don't treat stdlib specially in boot mode.Emilio Jesus Gallego Arias
This means the build system should pass the correct includes and library bindings to `coqdep`. We still have some discrepancies we won't be able to solve until `Loadpath` and `coqdep` are fused [which depends on the dune build.
2020-02-07[coqdep] Remove deprecated -slash , unused, undocumented -mldep option.Emilio Jesus Gallego Arias
2020-02-07[coqdep] Remove dumpgraph and broken optionsEmilio Jesus Gallego Arias
We remove the `dumpgraph` option which was causing quite a bit of duplication, we also clean up options marked as broken `-w/-D`
2020-02-07Merge PR #11543: restore the default URL for coquelicotThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-07restore the default URL for coquelicotYves Bertot
2020-02-06unsafe_type_of -> get_type_of in CcalgoGaëtan Gilbert
Not sure about these, let's see how it goes.
2020-02-06unsafe_type_of -> type_of in Cctac (with small refactor)Gaëtan Gilbert
Not sure if get_type_of would be fine, let's go with this for now.
2020-02-06unsafe_type_of -> get_type_of in Coq_omega.destructure_hypsGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Extractactics.destauto_inGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Extractactics.mkCaseEqGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.symmetry_inGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.default_morphismGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Rewrite.build_morphism_signatureGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Rewrite.resolve_morphismGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.decompose_app_relGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Firstorded.Instances.mk_open_instanceGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Sequent.extend_with_auto_hintsGaëtan Gilbert
+ fix evar leak in caller
2020-02-06unsafe_type_of -> type_of in Logic.check_typabilityGaëtan Gilbert
2020-02-06Remove Clenv.mk_clenv_type_of (hidden unsafe_type_of)Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Celenv.mk_clenv_type_ofGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in ComCoercion.build_id_coercionGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Auto_ind_decl.do_replace_blGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in ComProgramFixpoint.build_wellfoundedGaëtan Gilbert
We typecheck it literally the previous line...
2020-02-06unsafe_type_of -> get_type_of in Leminv.lemInvGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Equality.inject_if_homogenous_dependent_pairGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Equality.build_injrecGaëtan Gilbert
2020-02-06Remove useless unification in Equality.sig_clausal_formGaëtan Gilbert
We unify [w_type = type of w] with [a], but [w] was created with type [a]. This code was introduced in eab11e537905472fdcc3257bc9913df82c82b3e4 to fix #2255, AFAICT only the [minimal_free_rels_rec] part is necessary.
2020-02-06unsafe_type_of -> (get_)type_of in ↵Gaëtan Gilbert
Equality.{discrEq,minimal_free_rels_rec,sig_clausal_form}
2020-02-06unsafe_type_of -> get_type_of in Inv.raw_inversionGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Elim.induction_trailerGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 16:29:11 +0000