diff options
| author | Matthieu Sozeau | 2014-09-30 01:18:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-30 01:21:02 +0200 |
| commit | 2bbf1305a080667d8547c44b2684010aba3d8d45 (patch) | |
| tree | 42d2575fa01cc6f13eda2fb08ab26967f7834c04 /pretyping/reductionops.ml | |
| parent | 09d13ea251ba9f271fd698edd0d6560b88996a65 (diff) | |
Simplify evarconv thanks to new delta status of projections,
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 58d309997e..1131e81fef 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -189,7 +189,7 @@ module Cst_stack = struct let p_c = Termops.print_constr in prlist_with_sep pr_semicolon (fun (c,params,args) -> - hov 1 (p_c c ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++ + hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++ pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++ str ")")) l end @@ -329,7 +329,8 @@ struct | Cst_const (c1,u1), Cst_const (c2, u2) -> Constant.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj (p1,c1), Cst_proj (p2,c2) -> - Projection.equal p1 p2 && f (c1,lft1) (c2,lft2) + Constant.equal (Projection.constant p1) (Projection.constant p2) + && f (c1,lft1) (c2,lft2) | _, _ -> false in let rec equal_rec sk1 lft1 sk2 lft2 = @@ -838,7 +839,10 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let kn = Projection.constant p in let npars = pb.Declarations.proj_npars and arg = pb.Declarations.proj_arg in - match ReductionBehaviour.get (Globnames.ConstRef kn) with + if not tactic_mode then + let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in + whrec Cst_stack.empty stack' + else match ReductionBehaviour.get (Globnames.ConstRef kn) with | None -> let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in let stack'', csts = whrec Cst_stack.empty stack' in |