Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
N
Numerical Analysis in Coq
Manage
Activity
Members
Labels
Plan
Issues
0
Issue boards
Milestones
Wiki
Code
Merge requests
0
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Micaela Mayero
Numerical Analysis in Coq
Graph
a3e3422f676102dca0c593e2f7a62ac32fac9340
Select Git revision
Branches
6
Subset
essais-8.18
master
default
protected
pr_no_math-comp
released
test_skolem_ko
Tags
5
PhD_HM_2024
1.0
Bochner.1.0
Tonelli.1.0
LInt_p.1.0
11 results
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
16
Mar
15
14
12
11
10
9
8
7
6
5
4
3
2
1
28
Feb
27
26
25
24
23
22
21
20
19
18
17
16
15
14
13
12
11
10
9
8
7
6
5
4
3
2
1
31
Jan
30
29
28
27
24
23
22
21
20
19
18
17
16
15
14
13
11
10
9
8
21
Dec
20
19
18
17
16
15
14
13
12
10
Cosmetics: tuning expression of types of families of functions.
master
master
No need for parens.
New notations for smaller values.
Use new notations for ordinals.
Use new notation for ordinals in FEM.
Rm obsolete code.
Propagate new API (from multi_index).
Argument of CSdk is d1 and dimension is d=d1.+1.
Notation for [0..n] for [0..n.+1).
Add am_isobaryc{,_ms,_Rms}.
Add nat_sub_r_monot,
WIP: rev_insert_ord.
Rm useless.
Rename inj_CSdk_incr -> inj_CSdk_monot,
Hide unused.
Rename grsymlex_scal -> grsymlex_lt_mul.
Rename sum_mult -> sum_mul.
Generalize insert_ord_inj, insert_ord_neq_compat (n.+2 -> n.+1).
Go for higher level (constF, mapF).
Some cleaning of unused stuff.
Rm useless.
Modif node_ref, sub_vtx, sub_node.
Rename sub_nodeF -> sub_node_node,
WIP: get properties on sub_node from sub_node_ref.
Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis
Propagate new API.
Put structural parameters as first arguments.
MAJ html
Missing lemma inj_ASdki_incr
some proofs of MM and me about grsymlex
Argument K of kron becomes implicit.
Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis
Factor proofs of face unisolvence and 1st step of unisolvence.
Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis
modifs mineures
Factor proofs of face unisolvence.
Modif Hface_{0,S}_unisolvence.
Mv stuff around.
Cosmetics.
Add doc.
Loading