diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 15:50:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (patch) | |
| tree | 4ab6481d8d182f6bb3dd241b7112a3027aa26b2a /tactics/autorewrite.ml | |
| parent | ffb59901f568351401f2f3d1f3334031658b8880 (diff) | |
Removing some return type compatibility layers in Termops.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 029384297..f2e98ee01 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -286,7 +286,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) let t' = EConstr.Unsafe.to_constr t' in - match find_rel (it_mkProd_or_LetIn t' ctx) with + match find_rel (Term.it_mkProd_or_LetIn t' ctx) with | Some c -> Some c | None -> None |