summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_pretyping.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/subtac/subtac_pretyping.ml
parent55ce117e8083477593cf1ff2e51a3641c7973830 (diff)
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib/subtac/subtac_pretyping.ml')
-rw-r--r--contrib/subtac/subtac_pretyping.ml56
1 files changed, 28 insertions, 28 deletions
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 4d1ac731..cce9a358 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_pretyping.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
open Global
open Pp
@@ -36,7 +36,6 @@ open Subtac_utils
open Coqlib
open Printer
open Subtac_errors
-open Context
open Eterm
module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)
@@ -89,18 +88,18 @@ let list_split_at index l =
open Vernacexpr
-let coqintern evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
-let coqinterp evd env : Topconstr.constr_expr -> Term.constr = Constrintern.interp_constr (evars_of evd) env
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env
let env_with_binders env isevars l =
let rec aux ((env, rels) as acc) = function
Topconstr.LocalRawDef ((loc, name), def) :: tl ->
- let rawdef = coqintern !isevars env def in
+ let rawdef = coqintern_constr !isevars env def in
let coqdef, deftyp = interp env isevars rawdef empty_tycon in
let reldecl = (name, Some coqdef, deftyp) in
aux (push_rel reldecl env, reldecl :: rels) tl
| Topconstr.LocalRawAssum (bl, typ) :: tl ->
- let rawtyp = coqintern !isevars env typ in
+ let rawtyp = coqintern_type !isevars env typ in
let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
let acc =
List.fold_left (fun (env, rels) (loc, name) ->
@@ -113,36 +112,37 @@ let env_with_binders env isevars l =
in aux (env, []) l
let subtac_process env isevars id l c tycon =
- let env_binders, binders_rel = env_with_binders env isevars l in
+ let c = Command.abstract_constr_expr c l in
+(* let env_binders, binders_rel = env_with_binders env isevars l in *)
let tycon =
match tycon with
None -> empty_tycon
| Some t ->
- let t = coqintern !isevars env_binders t in
- let coqt, ttyp = interp env_binders isevars t empty_tycon in
+ let t = Command.generalize_constr_expr t l in
+ let t = coqintern_type !isevars env t in
+ let coqt, ttyp = interp env isevars t empty_tycon in
mk_tycon coqt
in
- let c = coqintern !isevars env_binders c in
- let c = Subtac_utils.rewrite_cases env c in
- let coqc, ctyp = interp env_binders isevars c tycon in
-(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ *)
-(* str "Coq type: " ++ my_print_constr env_binders ctyp) *)
-(* with _ -> () *)
+ let c = coqintern_constr !isevars env c in
+ let coqc, ctyp = interp env isevars c tycon in
+(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *)
+(* str "Coq type: " ++ my_print_constr env ctyp) *)
+(* with _ -> () *)
(* in *)
-(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in *)
+(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars)) with _ -> () in *)
- let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel
- and fullctyp = it_mkProd_or_LetIn ctyp binders_rel
- in
- let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in
- let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in
-
-(* let _ = try trace (str "After evar normalization: " ++ spc () ++ *)
-(* str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () *)
-(* ++ str "Coq type: " ++ my_print_constr env fullctyp) *)
-(* with _ -> () *)
+(* let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel *)
+(* and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *)
(* in *)
- let evm = non_instanciated_map env isevars in
+ let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in
+ let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in
+(* let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *)
+(* let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *)
+(* let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *)
+(* Evd.pr_evar_map evm) *)
+(* with _ -> () *)
+(* in *)
+ let evm = non_instanciated_map env isevars (evars_of !isevars) in
(* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
evm, fullcoqc, fullctyp
@@ -152,5 +152,5 @@ let subtac_proof env isevars id l c tycon =
let nc = named_context env in
let nc_len = named_context_length nc in
let evm, coqc, coqt = subtac_process env isevars id l c tycon in
- let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
+ let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in
add_definition id def coqt evars