diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-01 12:30:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-01 12:30:52 +0000 |
| commit | 5a87d97bd8bce29d3c94bd40e4ab03c4c7c098a8 (patch) | |
| tree | 3ad8750efcbc0bea1c4fc2dcbb57251391bf8a93 /contrib/funind | |
| parent | bd358a1f07807970bebf73f14f0ec941e34d9737 (diff) | |
Ajout possibilité clause "where" dans co-points fixes
(+ 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
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index a24e5845b..5f09b3590 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1194,11 +1194,10 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (dummy_loc,relnames.(i)), - None, + ((dummy_loc,relnames.(i)), rel_params, rel_arities.(i), - ext_rel_constructors + ext_rel_constructors),None in let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in let rel_inds = Array.to_list ext_rel_constructors in |