diff options
| author | letouzey | 2013-02-26 18:52:24 +0000 |
|---|---|---|
| committer | letouzey | 2013-02-26 18:52:24 +0000 |
| commit | 60de53d159c85b8300226a61aa502a7e0dd2f04b (patch) | |
| tree | e542ed90d58872a75816d451ae26e38fa7b1d9f9 /kernel/inductive.ml | |
| parent | 7dd28b4772251af6ae3641ec63a8251153915e21 (diff) | |
kernel/declarations becomes a pure mli
- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
- the functions that were in declarations.ml (mostly substitution utilities
and hashcons) are now in kernel/declareops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 31d9f48ac4..3132b7e796 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -12,6 +12,7 @@ open Names open Univ open Term open Declarations +open Declareops open Environ open Reduction open Type_errors @@ -414,8 +415,10 @@ type subterm_spec = | Dead_code | Not_subterm +let eq_wf_paths = Rtree.eq_rtree Declareops.eq_recarg + let spec_of_tree t = lazy - (if Rtree.eq_rtree eq_recarg (Lazy.force t) mk_norec + (if eq_wf_paths (Lazy.force t) mk_norec then Not_subterm else Subterm(Strict,Lazy.force t)) @@ -427,7 +430,7 @@ let subterm_spec_glb = | Not_subterm, _ -> Not_subterm | _, Not_subterm -> Not_subterm | Subterm (a1,t1), Subterm (a2,t2) -> - if Rtree.eq_rtree eq_recarg t1 t2 then Subterm (size_glb a1 a2, t1) + if eq_wf_paths t1 t2 then Subterm (size_glb a1 a2, t1) (* branches do not return objects with same spec *) else Not_subterm in Array.fold_left glb2 Dead_code @@ -877,7 +880,7 @@ let check_one_cofix env nbfix def deftype = let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> - if Rtree.eq_rtree eq_recarg rar mk_norec then + if eq_wf_paths rar mk_norec then if noccur_with_meta n nbfix t then process_args_of_constr (lr, lrar) else raise (CoFixGuardError |