diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-27 15:02:36 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-27 15:02:36 +0000 |
| commit | 023c516a2c0178f8e06b8ee795779fdd34aeba83 (patch) | |
| tree | ab032206f0aace5946061f574ad80bdd9df21bea /pretyping | |
| parent | 6da011a8677676462b24940a6171fb22615c3fbb (diff) | |
Closure optimizations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16937 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1cc9df024..4a188da00 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -457,7 +457,7 @@ let extract_conv_pbs evd p = pbs let extract_changed_conv_pbs evd p = - extract_conv_pbs evd (p evd.last_mods) + extract_conv_pbs evd (fun pb -> p evd.last_mods pb) let extract_all_conv_pbs evd = extract_conv_pbs evd (fun _ -> true) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5fb74dcad..6510655b9 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -895,11 +895,11 @@ let compare_constr_univ f cv_pb t1 t2 = Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 | Prod (_,t1,c1), Prod (_,t2,c2) -> f Reduction.CONV t1 t2 && f cv_pb c1 c2 - | _ -> compare_constr (f Reduction.CONV) t1 t2 + | _ -> compare_constr (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2 let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2 -let eq_constr = constr_cmp Reduction.CONV +let eq_constr t1 t2 = constr_cmp Reduction.CONV t1 t2 (* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn) App(c,[||]) -> ([],c) *) |