Commit 972195cb authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Why3 tactic: support for Prod (experimental)

parent 8bd7b8d1
......@@ -317,3 +317,11 @@ Goal wgt (S O, 3) = 3.
ae.
Qed.
Require Import BuiltIn.
Require Import R_sqrt.
Require Import Rfunctions.
Require Import Rbasic_fun.
Goal forall (x:R), (0 <= x * x)%R.
ae.
Qed.
......@@ -554,10 +554,22 @@ and tr_global_ts dep env r =
| _ -> raise NotFO (* GADT *)
in
List.fold_right2 add v ts.Ty.ts_args Idmap.empty
| Ind _ | Prod _ ->
Idmap.empty
| _ ->
assert false (* ensured by Coq typing *)
| Ind _ -> Idmap.empty
| Prod _ -> Idmap.empty
(* ensured by Coq typing *)
| CoFix _ -> assert false
| Fix _ -> assert false
| Case (_, _, _, _) -> assert false
| Construct _ -> assert false
| Const _ -> assert false
| LetIn (_, _, _, _) -> assert false
| Lambda (_, _, _) -> assert false
| Cast (_, _, _) -> assert false
| Sort _ -> assert false
| Evar _ -> assert false
| Meta _ -> assert false
| Var _ -> assert false
| Rel _ -> assert false
in
let l = List.map (tr_type dep' tvm env) l in
let id = preid_of_id (Nametab.basename_of_global r) in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment