Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 204 insertions, 133 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index df03a579..7d1f57fe 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -15,12 +15,6 @@ open Libnames;;
 open Goptions;;
 
 
-let in_coq_ref = ref false;;
-
-let declare_in_coq () = in_coq_ref:=true;;
-
-let in_coq () = !in_coq_ref;;
-
 (* // Verify whether this is dead code, as of coq version 7 *)
 (* The following three sentences have been added to cope with a change 
 of strategy from the Coq team in the way rules construct ast's.  The
@@ -203,6 +197,10 @@ let xlate_int_or_var_opt_to_int_opt = function
   | Some (ArgVar _) -> xlate_error "int_or_var: TODO"
   | None ->  CT_coerce_NONE_to_INT_OPT CT_none
 
+let apply_or_by_notation f = function
+  | AN x -> f x
+  | ByNotation _ -> xlate_error "TODO: ByNotation"
+
 let tac_qualid_to_ct_ID ref = 
   CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
 
@@ -307,14 +305,10 @@ let make_fix_struct (n,bl) =
   let names = names_of_local_assums bl in
   let nn = List.length names in
   if nn = 1 || n = None then ctv_ID_OPT_NONE
-  else 
-    let n = out_some n in 
-    if n < nn then xlate_id_opt(List.nth names n)
-    else xlate_error "unexpected result of parsing for Fixpoint";;
-
+  else ctf_ID_OPT_SOME(CT_ident (string_of_id (snd (Option.get n))));;
 
 let rec xlate_binder = function
-    (l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
+    (l,k,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
 and xlate_return_info = function
 | (Some Anonymous, None) | (None, None) ->
    CT_coerce_NONE_to_RETURN_INFO CT_none
@@ -327,7 +321,7 @@ and xlate_formula_opt =
     | Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e)
 
 and  xlate_binder_l = function
-    LocalRawAssum(l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
+    LocalRawAssum(l,_,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
   | LocalRawDef(n,v) -> CT_coerce_DEF_to_BINDER(CT_def(xlate_id_opt n,
 						       xlate_formula v))
 and 
@@ -336,7 +330,7 @@ and
   | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a, 
                                      List.map xlate_match_pattern l)
 and  translate_one_equation = function
-    (_,[lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
+    (_,[_,lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
   | _ -> xlate_error "TODO: disjunctive multiple patterns"
 and 
   xlate_binder_ne_list = function
@@ -379,8 +373,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		 (xlate_formula f, List.map xlate_formula_expl l'))
    | CApp(_, (_,f), l) -> 
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
-   | CCases (_, _, [], _) -> assert false
-   | CCases (_, ret_type, tm::tml, eqns)->
+   | CCases (_, _, _, [], _) -> assert false
+   | CCases (_, _, ret_type, tm::tml, eqns)->
        CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
 					   List.map xlate_matched_formula tml),
 		xlate_formula_opt ret_type,
@@ -418,23 +412,16 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
        CT_coerce_ID_to_FORMULA(CT_metaid (string_of_id s))
    | CPatVar (_, (true, s)) ->
        xlate_error "Second order variable not supported"
-   | CEvar (_, _) -> xlate_error "CEvar not supported"
+   | CEvar _ -> xlate_error "CEvar not supported"
    | CCoFix (_, (_, id), lm::lmi) -> 
-     let strip_mutcorec (fid, bl,arf, ardef) =
+     let strip_mutcorec ((_, fid), bl,arf, ardef) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       xlate_formula arf, xlate_formula ardef) in
         CT_cofixc(xlate_ident id,
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
    | CFix (_, (_, id), lm::lmi) ->       
-     let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
-        let (struct_arg,bl,arf,ardef) =
-	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
-	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
-         if bl = [] then
-	   let n = out_some n in 
-           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
-           (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
-         else (make_fix_struct (n, bl),bl,arf,ardef) in
+     let strip_mutrec ((_, fid), (n, ro), bl, arf, ardef) =
+        let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match xlate_binder_list bl with
@@ -461,7 +448,7 @@ and xlate_matched_formula = function
       CT_coerce_FORMULA_to_MATCHED_FORMULA(xlate_formula f)
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
-  | (a, Some (_,ExplByPos i)) -> 
+  | (a, Some (_,ExplByPos (i, _))) -> 
       xlate_error "explicitation of implicit by rank not supported"
   | (a, Some (_,ExplByName i)) ->
       CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a)
@@ -477,24 +464,31 @@ let (xlate_ident_or_metaid:
     AI (_, x) -> xlate_ident x
   | MetaId(_, x) -> CT_metaid x;;
 
+let nums_of_occs (b,nums) =
+  if b then nums
+  else List.map (function ArgArg x -> ArgArg (-x) | y -> y) nums
+
 let xlate_hyp = function
   | AI (_,id) -> xlate_ident id
   | MetaId _ -> xlate_error "MetaId should occur only in quotations"
 
 let xlate_hyp_location =
  function
-  | (nums, AI (_,id)), InHypTypeOnly ->
-      CT_intype(xlate_ident id, nums_or_var_to_int_list nums)
-  | (nums, AI (_,id)), InHypValueOnly ->
-      CT_invalue(xlate_ident id, nums_or_var_to_int_list nums)
-  | ([], AI (_,id)), InHyp ->
+  | (occs, AI (_,id)), InHypTypeOnly ->
+      CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
+  | (occs, AI (_,id)), InHypValueOnly ->
+      CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs))
+  | (occs, AI (_,id)), InHyp when occs = all_occurrences_expr ->
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_coerce_ID_to_UNFOLD (xlate_ident id))
-  | (a::l, AI (_,id)), InHyp ->
+  | ((_,a::l as occs), AI (_,id)), InHyp ->
+      let nums = nums_of_occs occs in
+      let a = List.hd nums and l = List.tl nums in
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_unfold_occ (xlate_ident id, 
 			CT_int_ne_list(num_or_var_to_int a, 
                                        nums_or_var_to_int_list_aux l)))
+  | (_, AI (_,id)), InHyp -> xlate_error "Unused" (* (true,]) *)
   | (_, MetaId _),_ -> 
       xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
 
@@ -507,7 +501,7 @@ let xlate_clause cls =
       | Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in
   CT_clause
     (hyps_info, 
-     if cls.onconcl then 
+     if cls.concl_occs <> no_occurrences_expr then 
        CT_coerce_STAR_to_STAR_OPT CT_star
      else
        CT_coerce_NONE_to_STAR_OPT CT_none)
@@ -606,14 +600,15 @@ let strip_targ_intropatt =
     | _ -> xlate_error "strip_targ_intropatt";;
 
 let get_flag r =
-  let conv_flags, red_ids = 
+  let conv_flags, red_ids =
+    let csts = List.map (apply_or_by_notation tac_qualid_to_ct_ID) r.rConst in
     if r.rDelta then
-      [CT_delta], CT_unfbut (List.map tac_qualid_to_ct_ID r.rConst)
+      [CT_delta], CT_unfbut csts
     else
       (if r.rConst = []
       then (* probably useless: just for compatibility *) []
       else [CT_delta]),
-      CT_unf (List.map tac_qualid_to_ct_ID r.rConst) in
+      CT_unf csts in
   let conv_flags = if r.rBeta then CT_beta::conv_flags else conv_flags in
   let conv_flags = if r.rIota then CT_iota::conv_flags else conv_flags in
   let conv_flags = if r.rZeta then CT_zeta::conv_flags else conv_flags in
@@ -633,6 +628,8 @@ let rec xlate_intro_pattern =
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
   | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
+  | IntroFresh _ -> xlate_error "TODO: IntroFresh"
+  | IntroRewrite _ -> xlate_error "TODO: IntroRewrite"
 
 let compute_INV_TYPE = function
    FullInversionClear -> CT_inv_clear
@@ -663,7 +660,8 @@ let xlate_largs_to_id_opt largs =
     | _ -> assert false;;
 
 let xlate_int_or_constr = function
-    ElimOnConstr a -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a)
+    ElimOnConstr (a,NoBindings) -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a)
+  | ElimOnConstr _ -> xlate_error "TODO: ElimOnConstr with bindings"
   | ElimOnIdent(_,i) ->
       CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
       	(CT_coerce_ID_to_ID_OR_INT(xlate_ident i))
@@ -676,9 +674,13 @@ let xlate_using = function
   | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);;
 
 let xlate_one_unfold_block = function
-    ([],qid) -> CT_coerce_ID_to_UNFOLD(tac_qualid_to_ct_ID qid)
-  | (n::nums, qid) ->
-      CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_or_var_to_int_ne_list n nums)
+    ((true,[]),qid) -> 
+      CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid)
+  | (((_,_::_) as occs), qid) ->
+      let l = nums_of_occs occs in
+      CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid, 
+                    nums_or_var_to_int_ne_list (List.hd l) (List.tl l))
+  | ((false,[]), qid) -> xlate_error "Unused"
 ;;
 
 let xlate_with_names = function
@@ -739,7 +741,8 @@ and xlate_red_tactic =
   | CbvVm -> CT_cbvvm
   | Hnf -> CT_hnf
   | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
-  | Simpl (Some (l,c)) -> 
+  | Simpl (Some (occs,c)) -> 
+      let l = nums_of_occs occs in
       CT_simpl 
 	(CT_coerce_PATTERN_to_PATTERN_OPT
 	   (CT_pattern_occ
@@ -758,9 +761,9 @@ and xlate_red_tactic =
   | Fold formula_list -> 
       CT_fold(CT_formula_list(List.map xlate_formula formula_list))
   | Pattern l ->
-     let pat_list = List.map (fun (nums,c) ->
+     let pat_list = List.map (fun (occs,c) ->
           CT_pattern_occ
-           (CT_int_list (nums_or_var_to_int_list_aux nums),
+           (CT_int_list (nums_or_var_to_int_list_aux (nums_of_occs occs)),
             xlate_formula c)) l in
      (match pat_list with
       | first :: others -> CT_pattern (CT_pattern_ne_list (first, others))
@@ -770,21 +773,23 @@ and xlate_red_tactic =
 and xlate_local_rec_tac = function 
  (* TODO LATER: local recursive tactics and global ones should be handled in
     the same manner *)
-  | ((_,x),(argl,tac)) ->
+  | ((_,x),Tacexp (TacFun (argl,tac))) ->
       let fst, rest = xlate_largs_to_id_opt argl in
 	CT_rec_tactic_fun(xlate_ident x,
 			  CT_id_opt_ne_list(fst, rest),
 			  xlate_tactic tac)
+  | _ -> xlate_error "TODO: more general argument of 'let rec in'"
 
 and xlate_tactic =
  function
    | TacFun (largs, t) ->
        let fst, rest =  xlate_largs_to_id_opt largs in
        CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t)
-   | TacThen (t1,t2) -> 
+   | TacThen (t1,[||],t2,[||]) -> 
        (match xlate_tactic t1 with
             CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
 	  | t -> CT_then (t,[xlate_tactic t2]))
+   | TacThen _ -> xlate_error "TacThen generalization TODO"
    | TacThens(t1,[]) -> assert false
    | TacThens(t1,t::l) ->
        let ct = xlate_tactic t in
@@ -831,36 +836,31 @@ and xlate_tactic =
    | TacMatchContext (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacLetIn (l, t) ->
+   | TacLetIn (false, l, t) ->
        let cvt_clause =
          function
-             ((_,s),None,ConstrMayEval v) ->
+             ((_,s),ConstrMayEval v) ->
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_DEF_BODY_to_LET_VALUE
                                (formula_to_def_body v))
-           | ((_,s),None,Tacexp t) -> 
+           | ((_,s),Tacexp t) -> 
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
                                (xlate_tactic t))
-           | ((_,s),None,t) -> 
+           | ((_,s),t) -> 
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
-                               (xlate_call_or_tacarg t))
-           | ((_,s),Some c,t) -> 
-	       CT_let_clause(xlate_ident s,
-			     CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic c),
-                               CT_coerce_TACTIC_COM_to_LET_VALUE
-				 (xlate_call_or_tacarg t)) in
+                               (xlate_call_or_tacarg t)) in
          let cl_l = List.map cvt_clause l in
          (match cl_l with
             | [] -> assert false 
             | fst::others ->
                 CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t))
-   | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition"
-   | TacLetRecIn(f1::l, t) -> 
+   | TacLetIn(true, [], _) -> xlate_error "recursive definition with no definition"
+   | TacLetIn(true, f1::l, t) -> 
        let tl =  CT_rec_tactic_fun_list
 		   (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
        CT_rec_tactic_in(tl, xlate_tactic t)
@@ -917,6 +917,7 @@ and xlate_tac =
     | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
     | TacChange (Some(l,c), f, b) -> 
 	(* TODO LATER: combine with other constructions of pattern_occ *)
+	let l = nums_of_occs l in
 	CT_change_local(
 	  CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l), 
 			 xlate_formula c),
@@ -946,18 +947,22 @@ and xlate_tac =
 	xlate_error "TODO: injection as"
     | TacFix (idopt, n) ->
      CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list [])
-    | TacMutualFix (id, n, fixtac_list) ->
+    | TacMutualFix (false, id, n, fixtac_list) ->
      let f (id,n,c) = CT_fixtac (xlate_ident id, CT_int n, xlate_formula c) in
      CT_fixtactic
       (ctf_ID_OPT_SOME (xlate_ident id), CT_int n,
       CT_fix_tac_list (List.map f fixtac_list))
+    | TacMutualFix (true, id, n, fixtac_list) ->
+        xlate_error "TODO: non user-visible fix"
     | TacCofix idopt ->
        CT_cofixtactic (xlate_ident_opt idopt, CT_cofix_tac_list [])
-    | TacMutualCofix (id, cofixtac_list) ->
+    | TacMutualCofix (false, id, cofixtac_list) ->
      let f (id,c) = CT_cofixtac (xlate_ident id, xlate_formula c) in
      CT_cofixtactic
       (CT_coerce_ID_to_ID_OPT (xlate_ident id),
       CT_cofix_tac_list (List.map f cofixtac_list))
+    | TacMutualCofix (true, id, cofixtac_list) ->
+        xlate_error "TODO: non user-visible cofix"
     | TacIntrosUntil (NamedHyp id) -> 
 	CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
     | TacIntrosUntil (AnonHyp n) -> 
@@ -975,10 +980,12 @@ and xlate_tac =
     | TacIntroMove (Some id, None) ->
      CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
     | TacIntroMove (None, None) ->  CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
-    | TacLeft bindl -> CT_left (xlate_bindings bindl)
-    | TacRight bindl -> CT_right (xlate_bindings bindl)
-    | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
-    | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
+    | TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
+    | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
+    | TacSplit (false,true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacSplit _ | TacRight _ | TacLeft _ -> 
+	xlate_error "TODO: esplit, eright, etc"
     | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
 	let c1 = xlate_formula (out_gen rawwit_constr c1) in
 	let c2 = xlate_formula (out_gen rawwit_constr c2) in
@@ -991,7 +998,7 @@ and xlate_tac =
 	  let cl_as_xlate_arg = 
 	    {cl_as_clause with 
 	       Tacexpr.onhyps = 
-		option_map 
+		Option.map 
 		  (fun l -> 
 		     List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l
 		  )
@@ -1009,12 +1016,15 @@ and xlate_tac =
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
 	CT_replace_with (c1, c2,cl,tac_opt)
-    | TacRewrite(b,cbindl,cl) -> 
+    | TacRewrite(false,[b,Precisely 1,cbindl],cl,None) -> 
      let cl = xlate_clause cl 
      and c = xlate_formula (fst cbindl) 
      and bindl = xlate_bindings (snd cbindl) in
      if b then CT_rewrite_lr (c, bindl, cl)
      else CT_rewrite_rl (c, bindl, cl)
+    | TacRewrite(_,_,_,Some _) -> xlate_error "TODO: rewrite by"
+    | TacRewrite(false,_,cl,_) -> xlate_error "TODO: rewrite of several hyps at once"
+    | TacRewrite(true,_,cl,_) -> xlate_error "TODO: erewrite"
     | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_main_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
@@ -1127,10 +1137,9 @@ and xlate_tac =
       (match out_gen rawwit_int_or_var n with
 	| ArgVar _ -> xlate_error ""
 	| ArgArg n -> CT_prolog (CT_formula_list cl, CT_int  n))
-    | TacExtend (_,"eapply", [cbindl]) ->
-     let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
-     let c = xlate_formula c and bindl = xlate_bindings bindl in
-     CT_eapply (c, bindl)
+    (* eapply now represented by TacApply (true,cbindl) 
+    | TacExtend (_,"eapply", [cbindl]) -> 
+*)
     | TacTrivial ([],Some []) -> CT_trivial
     | TacTrivial ([],None) -> 
 	CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
@@ -1141,25 +1150,36 @@ and xlate_tac =
 	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
-    | TacApply (c,bindl) ->
+    | TacApply (true,false,(c,bindl)) ->
      CT_apply (xlate_formula c, xlate_bindings bindl)
-    | TacConstructor (n_or_meta, bindl) ->
+    | TacApply (true,true,(c,bindl)) ->
+     CT_eapply (xlate_formula c, xlate_bindings bindl)
+    | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
+    | TacConstructor (false,n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
+    | TacConstructor _ -> xlate_error "TODO: econstructor"
     | TacSpecialize (nopt, (c,sl)) ->
      CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl)
     | TacGeneralize [] -> xlate_error ""
-    | TacGeneralize (first :: cl) ->
+    | TacGeneralize ((((true,[]),first),Anonymous) :: cl)
+	when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr
+	  & na = Anonymous) cl ->
      CT_generalize
-      (CT_formula_ne_list (xlate_formula first, List.map xlate_formula cl))
+      (CT_formula_ne_list (xlate_formula first, 
+                           List.map (fun ((_,c),_) -> xlate_formula c) cl))
+    | TacGeneralize _ -> xlate_error "TODO: Generalize at and as"
     | TacGeneralizeDep c ->
 	CT_generalize_dependent (xlate_formula c)
     | TacElimType c -> CT_elim_type (xlate_formula c)
     | TacCaseType c -> CT_case_type (xlate_formula c)
-    | TacElim ((c1,sl), u) ->
+    | TacElim (false,(c1,sl), u) ->
      CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
-    | TacCase (c1,sl) ->
+    | TacCase (false,(c1,sl)) ->
      CT_casetac (xlate_formula c1, xlate_bindings sl)
+    | TacElim (true,_,_) | TacCase (true,_)
+    | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) ->
+	xlate_error "TODO: eelim, ecase, edestruct, einduction"
     | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
     | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
     | TacCut c -> CT_cut (xlate_formula c)
@@ -1167,8 +1187,8 @@ and xlate_tac =
     | TacDecompose ([],c) ->
 	xlate_error "Decompose : empty list of identifiers?"
     | TacDecompose (id::l,c) ->
-	let id' = tac_qualid_to_ct_ID id in
-	let l' = List.map tac_qualid_to_ct_ID l in
+	let id' = apply_or_by_notation tac_qualid_to_ct_ID id in
+	let l' = List.map (apply_or_by_notation tac_qualid_to_ct_ID) l in
         CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
     | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
     | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
@@ -1178,6 +1198,7 @@ and xlate_tac =
        let idl' = List.map xlate_hyp idl in
        CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
     | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
+    | TacRevert _ -> xlate_error "TODO: revert"
     | (*For translating tactics/Inv.v *)
       TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
 	CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
@@ -1192,30 +1213,36 @@ and xlate_tac =
 	  CT_use_inversion (id, xlate_formula c,
 	    CT_id_list (List.map xlate_hyp idlist))
     | TacExtend (_,"omega", []) -> CT_omega
-    | TacRename (id1, id2) -> CT_rename(xlate_hyp id1, xlate_hyp id2)
+    | TacRename [id1, id2] -> CT_rename(xlate_hyp id1, xlate_hyp id2)
+    | TacRename _ -> xlate_error "TODO: add support for n-ary rename"
     | TacClearBody([]) -> assert false
     | TacClearBody(a::l) -> 
 	CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
-    | TacDAuto (a, b) ->
+    | TacDAuto (a, b, []) ->
 	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
-    | TacNewDestruct(a,b,c) ->
-	CT_new_destruct (* Julien F. : est-ce correct *)
+    | TacDAuto (a, b, _) ->
+	xlate_error "TODO: dauto using"
+    | TacNewDestruct(false,a,b,c,None) ->
+	CT_new_destruct
 	  (List.map  xlate_int_or_constr a, xlate_using b, 
 	   xlate_with_names c)
-    | TacNewInduction(a,b,c) ->
-	CT_new_induction (* Pierre C. : est-ce correct *)
+    | TacNewInduction(false,a,b,c,None) ->
+	CT_new_induction
 	  (List.map xlate_int_or_constr a, xlate_using b,
 	   xlate_with_names c)
+    | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in"
+    | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in"
     (*| TacInstantiate (a, b, cl) -> 
         CT_instantiate(CT_int a, xlate_formula b,
 		       assert false) *)
-    | TacLetTac (na, c, cl) when cl = nowhere -> 
+    | TacLetTac (na, c, cl, true) when cl = nowhere -> 
         CT_pose(xlate_id_opt_aux na, xlate_formula c)
-    | TacLetTac (na, c, cl) ->
+    | TacLetTac (na, c, cl, true) ->
         CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
 		  xlate_clause cl)
+    | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
     | TacAssert (None, IntroIdentifier id, c) -> 
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
     | TacAssert (None, IntroAnonymous, c) -> 
@@ -1226,16 +1253,18 @@ and xlate_tac =
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
-    | TacAnyConstructor(Some tac) -> 
+    | TacAnyConstructor(false,Some tac) -> 
 	CT_any_constructor
 	(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
-    | TacAnyConstructor(None) -> 
+    | TacAnyConstructor(false,None) -> 
 	CT_any_constructor(CT_coerce_NONE_to_TACTIC_OPT CT_none)
+    | TacAnyConstructor _ -> xlate_error "TODO: econstructor"
     | TacExtend(_, "ring", [args]) -> 
 	CT_ring
 	  (CT_formula_list
 	     (List.map xlate_formula
 		(out_gen (wit_list0 rawwit_constr) args)))
+    | TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal"
     | TacExtend (_,id, l) ->
 	print_endline ("Extratactics : "^ id);
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
@@ -1299,7 +1328,7 @@ and coerce_genarg_to_TARG x =
 					 (snd (out_gen
 					    (rawwit_open_constr_gen b) x))))
   | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
-      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let n = Option.get (Pcoq.tactic_genarg_level s) in
       let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_COM_to_TARG t
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
@@ -1392,7 +1421,7 @@ let coerce_genarg_to_VARG x =
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
   | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
-      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let n = Option.get (Pcoq.tactic_genarg_level s) in
       let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
   | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
@@ -1563,7 +1592,9 @@ let rec xlate_module_type = function
 	   | CWith_Module((_, idl), (_, qid)) ->
 	       CT_module_type_with_mod(mty1,
 				       CT_id_list (List.map xlate_ident idl), 
-				       CT_ident (xlate_qualid qid)));;
+				       CT_ident (xlate_qualid qid)))
+  | CMTEapply (_,_) -> xlate_error "TODO: Funsig application";;
+
 
 let xlate_module_binder_list (l:module_binder list) =
   CT_module_binder_list
@@ -1596,8 +1627,8 @@ let rec xlate_vernac =
    | VernacDeclareTacticDefinition (true, tacs) ->
        (match List.map 
 	 (function
-	      ((_, id), body) ->
-		CT_tac_def(CT_ident (string_of_id id), xlate_tactic body))
+	      (id, _, body) ->
+		CT_tac_def(reference_to_ct_ID id, xlate_tactic body))
 	 tacs with
 	     [] -> assert false
 	   | fst::tacs1 ->
@@ -1714,7 +1745,7 @@ let rec xlate_vernac =
 		      CT_id_ne_list(n1, names), dblist)
 	| HintsExtern (n, c, t) ->
 	    CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
-        | HintsResolve l | HintsImmediate l -> 
+        | HintsImmediate l -> 
 	 let f1, formulas = match List.map xlate_formula l with
 	     a :: tl -> a, tl
 	   | _  -> failwith "" in
@@ -1731,6 +1762,23 @@ let rec xlate_vernac =
 		  HintsResolve _ -> CT_hints_resolve(l', dblist)
 		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
 		| _ -> assert false)
+        | HintsResolve l -> 
+	 let f1, formulas = match List.map xlate_formula (List.map snd l) with
+	     a :: tl -> a, tl
+	   | _  -> failwith "" in
+	 let l' = CT_formula_ne_list(f1, formulas) in
+	   if local then
+             (match h with 
+		  HintsResolve _ ->
+		    CT_local_hints_resolve(l', dblist)
+	       	| HintsImmediate _ ->
+		    CT_local_hints_immediate(l', dblist)
+	       	| _ -> assert false)
+	   else
+	     (match h with
+		  HintsResolve _ -> CT_hints_resolve(l', dblist)
+		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
+		| _ -> assert false)
         | HintsUnfold l -> 
 	 let n1, names = match List.map loc_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
@@ -1766,13 +1814,11 @@ let rec xlate_vernac =
        ctf_ID_OPT_SOME (xlate_ident s))
   | VernacEndProof Admitted ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Admitted"), ctv_ID_OPT_NONE)
-  | VernacSetOpacity (false, id :: idl) ->
-            CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id,
-                   List.map loc_qualid_to_ct_ID idl))
-  | VernacSetOpacity (true, id :: idl)
-            -> CT_opaque (CT_id_ne_list(loc_qualid_to_ct_ID id,
-                   List.map loc_qualid_to_ct_ID idl))
-  | VernacSetOpacity (_, []) -> xlate_error "Shouldn't occur"
+  | VernacSetOpacity (_,l) ->
+      CT_strategy(CT_level_list
+        (List.map (fun (l,q) ->
+          (level_to_ct_LEVEL l,
+           CT_id_list(List.map loc_qualid_to_ct_ID q))) l))
   | VernacUndo n -> CT_undo (CT_coerce_INT_to_INT_OPT (CT_int n))
   | VernacShow (ShowGoal nopt) -> CT_show_goal (xlate_int_opt nopt)
   | VernacShow ShowNode -> CT_show_node
@@ -1799,7 +1845,7 @@ let rec xlate_vernac =
 	| PrintOpaqueName id -> CT_print_opaqueid (loc_qualid_to_ct_ID id)
 	| PrintSectionContext id -> CT_print_section (loc_qualid_to_ct_ID id)
 	| PrintModules -> CT_print_modules
-	| PrintGrammar (phylum, name) -> CT_print_grammar CT_grammar_none
+	| PrintGrammar name -> CT_print_grammar CT_grammar_none
 	| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
 	| PrintHintDbName id -> 
 	    CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
@@ -1819,6 +1865,12 @@ let rec xlate_vernac =
 	    CT_print_path (xlate_class id1, xlate_class id2)
 	| PrintCanonicalConversions ->
 	    xlate_error "TODO: Print Canonical Structures"
+	| PrintAssumptions _ -> 
+	    xlate_error "TODO: Print Needed Assumptions"
+	| PrintInstances _ -> 
+	    xlate_error "TODO: Print Instances"
+	| PrintTypeClasses -> 
+	    xlate_error "TODO: Print TypeClasses"
 	| PrintInspect n -> CT_inspect (CT_int n)
 	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
 	| PrintSetoids -> CT_print_setoids
@@ -1837,12 +1889,14 @@ let rec xlate_vernac =
   | VernacBeginSection (_,id) ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
-  | VernacStartTheoremProof (k, (_,s), (bl,c), _, _) ->
+  | VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND(
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
            xlate_binder_list bl, xlate_formula c))
+  | VernacStartTheoremProof _ ->
+      xlate_error "TODO: Mutually dependent theorems"
   | VernacSuspend -> CT_suspend
-  | VernacResume idopt -> CT_resume (xlate_ident_opt (option_map snd idopt))
+  | VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt))
   | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND
 	(CT_theorem_goal
@@ -1853,8 +1907,9 @@ let rec xlate_vernac =
 	(xlate_defn kind, xlate_ident s, xlate_binder_list bl,
 	   cvt_optional_eval_for_definition c red_option,
            xlate_formula_opt typ_opt)
-  | VernacAssumption (kind, b) ->
-      CT_variable (xlate_var kind, cvt_vernac_binders b)
+  | VernacAssumption (kind,inline ,b) ->xlate_error "TODO: Parameter Inline"
+      (*inline : bool -> automatic delta reduction at fonctor application*)
+     (* CT_variable (xlate_var kind, cvt_vernac_binders b)*)
   | VernacCheckMayEval (None, numopt, c) ->
       CT_check (xlate_formula c)
   | VernacSearch (s,x) ->
@@ -1884,7 +1939,7 @@ let rec xlate_vernac =
       (_, (add_coercion, (_,s)), binders, c1,
        rec_constructor_or_none, field_list) ->
       let record_constructor =
-        xlate_ident_opt (option_map snd rec_constructor_or_none) in
+        xlate_ident_opt (Option.map snd rec_constructor_or_none) in
       CT_record
        ((if add_coercion then CT_coercion_atm else
           CT_coerce_NONE_to_COERCION_OPT(CT_none)),
@@ -1902,15 +1957,8 @@ let rec xlate_vernac =
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
    | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
    | VernacFixpoint ((lm :: lmi),boxed) ->
-      let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) =
-        let (struct_arg,bl,arf,ardef) =
-	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
-	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
-         if bl = [] then
-	   let n = out_some n in 
-           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
-           (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
-         else (make_fix_struct (n, bl),bl,arf,ardef) in
+      let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) =
+        let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match xlate_binder_list bl with
@@ -1922,26 +1970,35 @@ let rec xlate_vernac =
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
    | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
    | VernacCoFixpoint ((lm :: lmi),boxed) ->
-      let strip_mutcorec ((fid, bl, arf, ardef), _ntn) =
+      let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       xlate_formula arf, xlate_formula ardef) in
         CT_cofix_decl
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
    | VernacScheme [] -> xlate_error "induction scheme"
    | VernacScheme (lm :: lmi) ->
-      let strip_ind ((_,id), depstr, inde, sort) =
+      let strip_ind = function
+      | (Some (_,id), InductionScheme (depstr, inde, sort)) ->
            CT_scheme_spec
             (xlate_ident id, xlate_dep depstr, 
 	    CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
-	     xlate_sort sort) in
+	     xlate_sort sort)
+      | (None, InductionScheme (depstr, inde, sort)) ->
+           CT_scheme_spec
+            (xlate_ident (id_of_string ""), xlate_dep depstr,
+            CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
+             xlate_sort sort)
+      | (_, EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in
         CT_ind_scheme
 	  (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
-   | VernacSyntacticDefinition (id, c, false, _) ->
+   | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme"
+   | VernacSyntacticDefinition ((_,id), ([],c), false, _) ->
        CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None)
-   | VernacSyntacticDefinition (id, c, true, _) ->
-       xlate_error "TODO: Local abbreviations"
+   | VernacSyntacticDefinition ((_,id), _, _, _) ->
+       xlate_error"TODO: Local abbreviations and abbreviations with parameters"
   (* Modules and Module Types *)
-  | VernacDeclareModuleType((_, id), bl, mty_o)  -> 
+   | VernacInclude (_) -> xlate_error "TODO : Include "
+   | VernacDeclareModuleType((_, id), bl, mty_o)  -> 
       CT_module_type_decl(xlate_ident id,
 			  xlate_module_binder_list bl,
 			  match mty_o with
@@ -2051,6 +2108,12 @@ let rec xlate_vernac =
        | Local -> CT_local in
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
+
+    (* Type Classes *) 
+   | VernacDeclareInstance _|VernacContext _|
+	 VernacInstance (_, _, _, _, _)|VernacClass (_, _, _, _, _) ->
+	   xlate_error "TODO: Type Classes commands"
+
   | VernacResetName id -> CT_reset (xlate_ident (snd id))
   | VernacResetInitial -> CT_restore_state (CT_ident "Initial")
   | VernacExtend (s, l) ->
@@ -2073,10 +2136,10 @@ let rec xlate_vernac =
 	       CT_coerce_ID_LIST_to_ID_LIST_OPT
 	       (CT_id_list
 	       (List.map
-		  (function ExplByPos x
+		  (function ExplByPos (x,_), _, _
 		       -> xlate_error
 			   "explication argument by rank is obsolete"
-		     | ExplByName id -> CT_ident (string_of_id id)) l)))
+		     | ExplByName id, _, _ -> CT_ident (string_of_id id)) l)))
   | VernacDeclareImplicits(false, id, opt_positions) ->
       xlate_error "TODO: Implicit Arguments Global"
   | VernacReserve((_,a)::l, f) ->
@@ -2096,13 +2159,15 @@ let rec xlate_vernac =
       let table1 = 
 	match table with
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
+	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
 	CT_set_option(table1)
   | VernacSetOption (table, v) -> 
       let table1 = 
 	match table with
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
+	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
       let value =
 	match v with
 	  | BoolValue _ -> assert false
@@ -2115,7 +2180,8 @@ let rec xlate_vernac =
       let table1 = 
 	match table with
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
+	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
 	CT_unset_option(table1)
   | VernacAddOption (table, l) ->
       let values =
@@ -2130,7 +2196,8 @@ let rec xlate_vernac =
       let table1 = 
 	match table with
 	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
+	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
 	CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1))
   | VernacImport(true, a::l) ->
       CT_export_id(CT_id_ne_list(reference_to_ct_ID a,
@@ -2140,13 +2207,17 @@ let rec xlate_vernac =
 				 List.map reference_to_ct_ID l))
   | VernacImport(_, []) -> assert false
   | VernacProof t -> CT_proof_with(xlate_tactic t)
-  | VernacVar _ -> xlate_error "Grammar vernac obsolete"
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)
   | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
     VernacSolveExistential (_, _)|VernacCanonical _ |
-     VernacTacticNotation _)
-    -> xlate_error "TODO: vernac";;
+     VernacTacticNotation _ | VernacUndoTo _ | VernacRemoveName _)
+    -> xlate_error "TODO: vernac"
+and level_to_ct_LEVEL = function
+    Conv_oracle.Opaque -> CT_Opaque
+  | Conv_oracle.Level n -> CT_Level (CT_int n)
+  | Conv_oracle.Expand -> CT_Expand;;
+
 
 let rec xlate_vernac_list =
  function