diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 03:04:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:31 +0100 |
| commit | d833b81b49366e95cf20a1d00f9c63883adb8942 (patch) | |
| tree | 1afca49fcd42e96b658c90d28e9da692ccc39724 /plugins/decl_mode | |
| parent | c0d38ae52ac410811e7df54c52e8d3a18bb11bcb (diff) | |
Rewrite API using EConstr.
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 54206aa95..5de2c4151 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -382,6 +382,9 @@ let enstack_subsubgoals env se stack gls= Array.iteri process gentypes | _ -> () +let nf_meta sigma c = + EConstr.Unsafe.to_constr (Reductionops.nf_meta sigma (EConstr.of_constr c)) + let rec nf_list evd = function [] -> [] @@ -389,7 +392,7 @@ let rec nf_list evd = if meta_defined evd m then nf_list evd others else - (m,Reductionops.nf_meta evd typ)::nf_list evd others + (m,nf_meta evd typ)::nf_list evd others let find_subsubgoal c ctyp skip submetas gls = let env= pf_env gls in @@ -424,7 +427,7 @@ let find_subsubgoal c ctyp skip submetas gls = dfs n end in let nse= try dfs skip with Stack.Empty -> raise Not_found in - nf_list nse.se_evd nse.se_meta_list,Reductionops.nf_meta nse.se_evd (mkMeta 0) + nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0) let concl_refiner metas body gls = let concl = pf_concl gls in |