Quelle  ltac2_check_globalize.out   Sprache: unbekannt

()
() : unit
fun x => x : 'a -> 'a
() ()
(1, 2) 3
let x := () in
x ()
File "./output/ltac2_check_globalize.v", line 22, characters 32-33:
The command has indeed failed with message:
This expression has type unit. It is not a function and cannot be applied.
let x := fun x => x in
let _ := x 1 in
let _ := x "" in
()
let x := fun x => x in
let _ := x 1 in
let _ := x "" in
() : unit
let accu := { contents := []} in
(let x := fun x => accu.(contents) := (x :: accu.(contents)) in
 let _ := x 1 in
 let _ := x "" in
 ());
accu.(contents)
File "./output/ltac2_check_globalize.v", line 38, characters 0-144:
The command has indeed failed with message:
This expression has type string but an expression was expected of type 
int
let (m : '__α Pattern.goal_matching) :=
  ([(([(None, (Pattern.MatchPattern, pat:(_)))],
      (Pattern.MatchPattern, pat:(_))),
     (fun h =>
      let h := Array.get h 0 in
      fun _ => fun _ => fun _ => fun _ => Std.clear h));
     (([], (Pattern.MatchPattern, pat:(_))),
      (fun _ => fun _ => fun _ => fun _ => fun _ => ()))]
    : _ Pattern.goal_matching)
in
Pattern.lazy_goal_match0 false m :'__α
constr:(ltac2:(()))