diff options
| author | jforest | 2010-07-16 20:00:04 +0000 |
|---|---|---|
| committer | jforest | 2010-07-16 20:00:04 +0000 |
| commit | adf6390ab7bf96b0ffd699e96bd6b27bd9d99d98 (patch) | |
| tree | 7565397787178d5f70aaa79e4d8dafdd4bc6b933 /toplevel | |
| parent | fa50dd40b26000c0fe1083fc7c5e76d45ebe6261 (diff) | |
Amelioration dans Function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13292 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 9 | ||||
| -rw-r--r-- | toplevel/command.mli | 2 |
2 files changed, 6 insertions, 5 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 21fb277e2b..3fa83662b2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -593,15 +593,16 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns -let extract_decreasing_argument = function +let extract_decreasing_argument limit = function | (na,CStructRec) -> na + | (na,_) when not limit -> na | _ -> error "Only structural decreasing is supported for a non-Program Fixpoint" -let extract_fixpoint_components l = +let extract_fixpoint_components limit l = let fixl, ntnl = List.split l in let fixl = List.map (fun ((_,id),ann,bl,typ,def) -> - let ann = extract_decreasing_argument ann in + let ann = extract_decreasing_argument limit ann in {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in fixl, List.flatten ntnl @@ -612,7 +613,7 @@ let extract_cofixpoint_components l = List.flatten ntnl let do_fixpoint l b = - let fixl,ntns = extract_fixpoint_components l in + let fixl,ntns = extract_fixpoint_components true l in let fix = interp_fixpoint fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences (snd fix) in diff --git a/toplevel/command.mli b/toplevel/command.mli index 779e77f313..818b81ec69 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -103,7 +103,7 @@ type structured_fixpoint_expr = { (** Extracting the semantical components out of the raw syntax of (co)fixpoints declarations *) -val extract_fixpoint_components : +val extract_fixpoint_components : bool -> (fixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list |