diff options
Diffstat (limited to 'plugins/firstorder/formula.ml')
| -rw-r--r-- | plugins/firstorder/formula.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 047fc9fb..a60a966c 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -211,7 +211,7 @@ type left_pattern= | Lexists of pinductive | LA of constr*left_arrow_pattern -type t={id:global_reference; +type t={id:GlobRef.t; constr:constr; pat:(left_pattern,right_pattern) sum; atoms:atoms} |