diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 18:56:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 18:56:18 +0200 |
| commit | a52d06ea16cff00faa7d2f63ad5c1ca0b58e64b4 (patch) | |
| tree | 40440d7daed82bd24180b36ef224f245ddca42f5 /tactics/hipattern.ml | |
| parent | 30a908becf31d91592a1f7934cfa3df2d67d1834 (diff) | |
| parent | a321074cdd2f9375662c7c9f17be5c045328bd82 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 72c3523da..27af7200b 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -511,7 +511,7 @@ let coq_eqdec ~sum ~rev = let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in let args = [eqn; mkGAppRef coq_not_ref [eqn]] in let args = if rev then List.rev args else args in - mkPattern (mkGAppRef sum [eqn; mkGAppRef coq_not_ref [eqn]]) + mkPattern (mkGAppRef sum args) ) (** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *) |