diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 18:18:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 (patch) | |
| tree | ae729d05933776d718905029f0a87722716ec57f /pretyping/recordops.ml | |
| parent | 531590c223af42c07a93142ab0cea470a98964e6 (diff) | |
Ltac now uses evar-based constrs.
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 8362a2a26..bc9e3a1f4 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -191,7 +191,7 @@ let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (t,con_pp,proji_sp_pp) -> strbrk "Projection value has no head constant: " - ++ Termops.print_constr t ++ strbrk " in canonical instance " + ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) @@ -256,8 +256,8 @@ let add_canonical_structure warn o = in match ocs with | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table; | Some (c, cs) -> - let old_can_s = (Termops.print_constr cs.o_DEF) - and new_can_s = (Termops.print_constr s.o_DEF) in + let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF)) + and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) |